![]() |
Metamath
Proof Explorer Theorem List (p. 134 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | supxrmnf 13301 | Adding minus infinity to a set does not affect its supremum. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β sup((π΄ βͺ {-β}), β*, < ) = sup(π΄, β*, < )) | ||
Theorem | supxrpnf 13302 | The supremum of a set of extended reals containing plus infinity is plus infinity. (Contributed by NM, 15-Oct-2005.) |
β’ ((π΄ β β* β§ +β β π΄) β sup(π΄, β*, < ) = +β) | ||
Theorem | supxrunb1 13303* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ β€ π¦ β sup(π΄, β*, < ) = +β)) | ||
Theorem | supxrunb2 13304* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ < π¦ β sup(π΄, β*, < ) = +β)) | ||
Theorem | supxrbnd1 13305* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ < π₯ β sup(π΄, β*, < ) < +β)) | ||
Theorem | supxrbnd2 13306* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ β€ π₯ β sup(π΄, β*, < ) < +β)) | ||
Theorem | xrsup0 13307 | The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.) |
β’ sup(β , β*, < ) = -β | ||
Theorem | supxrub 13308 | A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006.) |
β’ ((π΄ β β* β§ π΅ β π΄) β π΅ β€ sup(π΄, β*, < )) | ||
Theorem | supxrlub 13309* | The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΅ < sup(π΄, β*, < ) β βπ₯ β π΄ π΅ < π₯)) | ||
Theorem | supxrleub 13310* | The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by NM, 22-Feb-2006.) (Revised by Mario Carneiro, 6-Sep-2014.) |
β’ ((π΄ β β* β§ π΅ β β*) β (sup(π΄, β*, < ) β€ π΅ β βπ₯ β π΄ π₯ β€ π΅)) | ||
Theorem | supxrre 13311* | The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005.) (Proof shortened by Mario Carneiro, 7-Sep-2014.) |
β’ ((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β sup(π΄, β*, < ) = sup(π΄, β, < )) | ||
Theorem | supxrbnd 13312 | The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.) |
β’ ((π΄ β β β§ π΄ β β β§ sup(π΄, β*, < ) < +β) β sup(π΄, β*, < ) β β) | ||
Theorem | supxrgtmnf 13313 | The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.) |
β’ ((π΄ β β β§ π΄ β β ) β -β < sup(π΄, β*, < )) | ||
Theorem | supxrre1 13314 | The supremum of a nonempty set of reals is real iff it is less than plus infinity. (Contributed by NM, 5-Feb-2006.) |
β’ ((π΄ β β β§ π΄ β β ) β (sup(π΄, β*, < ) β β β sup(π΄, β*, < ) < +β)) | ||
Theorem | supxrre2 13315 | The supremum of a nonempty set of reals is real iff it is not plus infinity. (Contributed by NM, 5-Feb-2006.) |
β’ ((π΄ β β β§ π΄ β β ) β (sup(π΄, β*, < ) β β β sup(π΄, β*, < ) β +β)) | ||
Theorem | supxrss 13316 | Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ ((π΄ β π΅ β§ π΅ β β*) β sup(π΄, β*, < ) β€ sup(π΅, β*, < )) | ||
Theorem | infxrcl 13317 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by NM, 19-Jan-2006.) (Revised by AV, 5-Sep-2020.) |
β’ (π΄ β β* β inf(π΄, β*, < ) β β*) | ||
Theorem | infxrlb 13318 | A member of a set of extended reals is greater than or equal to the set's infimum. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.) |
β’ ((π΄ β β* β§ π΅ β π΄) β inf(π΄, β*, < ) β€ π΅) | ||
Theorem | infxrgelb 13319* | The infimum of a set of extended reals is greater than or equal to a lower bound. (Contributed by Mario Carneiro, 16-Mar-2014.) (Revised by AV, 5-Sep-2020.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΅ β€ inf(π΄, β*, < ) β βπ₯ β π΄ π΅ β€ π₯)) | ||
Theorem | infxrre 13320* | The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 5-Sep-2020.) |
β’ ((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β inf(π΄, β*, < ) = inf(π΄, β, < )) | ||
Theorem | infxrmnf 13321 | The infinimum of a set of extended reals containing minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
β’ ((π΄ β β* β§ -β β π΄) β inf(π΄, β*, < ) = -β) | ||
Theorem | xrinf0 13322 | The infimum of the empty set under the extended reals is positive infinity. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 5-Sep-2020.) |
β’ inf(β , β*, < ) = +β | ||
Theorem | infxrss 13323 | Larger sets of extended reals have smaller infima. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.) |
β’ ((π΄ β π΅ β§ π΅ β β*) β inf(π΅, β*, < ) β€ inf(π΄, β*, < )) | ||
Theorem | reltre 13324* | For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β βπ¦ β β π¦ < π₯ | ||
Theorem | rpltrp 13325* | For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β+ βπ¦ β β+ π¦ < π₯ | ||
Theorem | reltxrnmnf 13326* | For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β* (-β < π₯ β βπ¦ β β π¦ < π₯) | ||
Theorem | infmremnf 13327 | The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020.) |
β’ inf(β, β*, < ) = -β | ||
Theorem | infmrp1 13328 | The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020.) |
β’ inf(β+, β, < ) = 0 | ||
Syntax | cioo 13329 | Extend class notation with the set of open intervals of extended reals. |
class (,) | ||
Syntax | cioc 13330 | Extend class notation with the set of open-below, closed-above intervals of extended reals. |
class (,] | ||
Syntax | cico 13331 | Extend class notation with the set of closed-below, open-above intervals of extended reals. |
class [,) | ||
Syntax | cicc 13332 | Extend class notation with the set of closed intervals of extended reals. |
class [,] | ||
Definition | df-ioo 13333* | Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ (,) = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) | ||
Definition | df-ioc 13334* | Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ (,] = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ β€ π¦)}) | ||
Definition | df-ico 13335* | Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ [,) = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π¦)}) | ||
Definition | df-icc 13336* | Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ [,] = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ β€ π¦)}) | ||
Theorem | ixxval 13337* | Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ ((π΄ β β* β§ π΅ β β*) β (π΄ππ΅) = {π§ β β* β£ (π΄π π§ β§ π§ππ΅)}) | ||
Theorem | elixx1 13338* | Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄ππ΅) β (πΆ β β* β§ π΄π πΆ β§ πΆππ΅))) | ||
Theorem | ixxf 13339* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ π:(β* Γ β*)βΆπ« β* | ||
Theorem | ixxex 13340* | The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ π β V | ||
Theorem | ixxssxr 13341* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ (π΄ππ΅) β β* | ||
Theorem | elixx3g 13342* | Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show π΄ β β* and π΅ β β*. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ (πΆ β (π΄ππ΅) β ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄π πΆ β§ πΆππ΅))) | ||
Theorem | ixxssixx 13343* | An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ π€ β β*) β (π΄π π€ β π΄ππ€)) & β’ ((π€ β β* β§ π΅ β β*) β (π€ππ΅ β π€ππ΅)) β β’ (π΄ππ΅) β (π΄ππ΅) | ||
Theorem | ixxdisj 13344* | Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΅ β β* β§ π€ β β*) β (π΅ππ€ β Β¬ π€ππ΅)) β β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β ((π΄ππ΅) β© (π΅ππΆ)) = β ) | ||
Theorem | ixxun 13345* | Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΅ β β* β§ π€ β β*) β (π΅ππ€ β Β¬ π€ππ΅)) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β* β§ πΆ β β*) β ((π€ππ΅ β§ π΅ππΆ) β π€ππΆ)) & β’ ((π΄ β β* β§ π΅ β β* β§ π€ β β*) β ((π΄ππ΅ β§ π΅ππ€) β π΄π π€)) β β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ππ΅ β§ π΅ππΆ)) β ((π΄ππ΅) βͺ (π΅ππΆ)) = (π΄ππΆ)) | ||
Theorem | ixxin 13346* | Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ πΆ β β* β§ π§ β β*) β (if(π΄ β€ πΆ, πΆ, π΄)π π§ β (π΄π π§ β§ πΆπ π§))) & β’ ((π§ β β* β§ π΅ β β* β§ π· β β*) β (π§πif(π΅ β€ π·, π΅, π·) β (π§ππ΅ β§ π§ππ·))) β β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄ππ΅) β© (πΆππ·)) = (if(π΄ β€ πΆ, πΆ, π΄)πif(π΅ β€ π·, π΅, π·))) | ||
Theorem | ixxss1 13347* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ π΅ β β* β§ π€ β β*) β ((π΄ππ΅ β§ π΅ππ€) β π΄π π€)) β β’ ((π΄ β β* β§ π΄ππ΅) β (π΅ππΆ) β (π΄ππΆ)) | ||
Theorem | ixxss2 13348* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β* β§ πΆ β β*) β ((π€ππ΅ β§ π΅ππΆ) β π€ππΆ)) β β’ ((πΆ β β* β§ π΅ππΆ) β (π΄ππ΅) β (π΄ππΆ)) | ||
Theorem | ixxss12 13349* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ πΆ β β* β§ π€ β β*) β ((π΄ππΆ β§ πΆππ€) β π΄π π€)) & β’ ((π€ β β* β§ π· β β* β§ π΅ β β*) β ((π€ππ· β§ π·ππ΅) β π€ππ΅)) β β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ππΆ β§ π·ππ΅)) β (πΆππ·) β (π΄ππ΅)) | ||
Theorem | ixxub 13350* | Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β*) β (π€ < π΅ β π€ππ΅)) & β’ ((π€ β β* β§ π΅ β β*) β (π€ππ΅ β π€ β€ π΅)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄ < π€ β π΄π π€)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄π π€ β π΄ β€ π€)) β β’ ((π΄ β β* β§ π΅ β β* β§ (π΄ππ΅) β β ) β sup((π΄ππ΅), β*, < ) = π΅) | ||
Theorem | ixxlb 13351* | Extract the lower bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by AV, 12-Sep-2020.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β*) β (π€ < π΅ β π€ππ΅)) & β’ ((π€ β β* β§ π΅ β β*) β (π€ππ΅ β π€ β€ π΅)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄ < π€ β π΄π π€)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄π π€ β π΄ β€ π€)) β β’ ((π΄ β β* β§ π΅ β β* β§ (π΄ππ΅) β β ) β inf((π΄ππ΅), β*, < ) = π΄) | ||
Theorem | iooex 13352 | The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ (,) β V | ||
Theorem | iooval 13353* | Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄(,)π΅) = {π₯ β β* β£ (π΄ < π₯ β§ π₯ < π΅)}) | ||
Theorem | ioo0 13354 | An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄(,)π΅) = β β π΅ β€ π΄)) | ||
Theorem | ioon0 13355 | An open interval of extended reals is nonempty iff the lower argument is less than the upper argument. (Contributed by NM, 2-Mar-2007.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄(,)π΅) β β β π΄ < π΅)) | ||
Theorem | ndmioo 13356 | The open interval function's value is empty outside of its domain. (Contributed by NM, 21-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (Β¬ (π΄ β β* β§ π΅ β β*) β (π΄(,)π΅) = β ) | ||
Theorem | iooid 13357 | An open interval with identical lower and upper bounds is empty. (Contributed by NM, 21-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ (π΄(,)π΄) = β | ||
Theorem | elioo3g 13358 | Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show π΄ β β* and π΅ β β*. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ (πΆ β (π΄(,)π΅) β ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | elioore 13359 | A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ (π΄ β (π΅(,)πΆ) β π΄ β β) | ||
Theorem | lbioo 13360 | An open interval does not contain its left endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ Β¬ π΄ β (π΄(,)π΅) | ||
Theorem | ubioo 13361 | An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ Β¬ π΅ β (π΄(,)π΅) | ||
Theorem | iooval2 13362* | Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄(,)π΅) = {π₯ β β β£ (π΄ < π₯ β§ π₯ < π΅)}) | ||
Theorem | iooin 13363 | Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄(,)π΅) β© (πΆ(,)π·)) = (if(π΄ β€ πΆ, πΆ, π΄)(,)if(π΅ β€ π·, π΅, π·))) | ||
Theorem | iooss1 13364 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.) |
β’ ((π΄ β β* β§ π΄ β€ π΅) β (π΅(,)πΆ) β (π΄(,)πΆ)) | ||
Theorem | iooss2 13365 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((πΆ β β* β§ π΅ β€ πΆ) β (π΄(,)π΅) β (π΄(,)πΆ)) | ||
Theorem | iocval 13366* | Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄(,]π΅) = {π₯ β β* β£ (π΄ < π₯ β§ π₯ β€ π΅)}) | ||
Theorem | icoval 13367* | Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ < π΅)}) | ||
Theorem | iccval 13368* | Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄[,]π΅) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ β€ π΅)}) | ||
Theorem | elioo1 13369 | Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄(,)π΅) β (πΆ β β* β§ π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | elioo2 13370 | Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄(,)π΅) β (πΆ β β β§ π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | elioc1 13371 | Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄(,]π΅) β (πΆ β β* β§ π΄ < πΆ β§ πΆ β€ π΅))) | ||
Theorem | elico1 13372 | Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,)π΅) β (πΆ β β* β§ π΄ β€ πΆ β§ πΆ < π΅))) | ||
Theorem | elicc1 13373 | Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ πΆ β§ πΆ β€ π΅))) | ||
Theorem | iccid 13374 | A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.) |
β’ (π΄ β β* β (π΄[,]π΄) = {π΄}) | ||
Theorem | ico0 13375 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄[,)π΅) = β β π΅ β€ π΄)) | ||
Theorem | ioc0 13376 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄(,]π΅) = β β π΅ β€ π΄)) | ||
Theorem | icc0 13377 | An empty closed interval of extended reals. (Contributed by FL, 30-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄[,]π΅) = β β π΅ < π΄)) | ||
Theorem | dfrp2 13378 | Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020.) |
β’ β+ = (0(,)+β) | ||
Theorem | elicod 13379 | Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ πΆ) & β’ (π β πΆ < π΅) β β’ (π β πΆ β (π΄[,)π΅)) | ||
Theorem | icogelb 13380 | An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄[,)π΅)) β π΄ β€ πΆ) | ||
Theorem | elicore 13381 | A member of a left-closed right-open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ πΆ β (π΄[,)π΅)) β πΆ β β) | ||
Theorem | ubioc1 13382 | The upper bound belongs to an open-below, closed-above interval. See ubicc2 13447. (Contributed by FL, 29-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β π΅ β (π΄(,]π΅)) | ||
Theorem | lbico1 13383 | The lower bound belongs to a closed-below, open-above interval. See lbicc2 13446. (Contributed by FL, 29-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β π΄ β (π΄[,)π΅)) | ||
Theorem | iccleub 13384 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄[,]π΅)) β πΆ β€ π΅) | ||
Theorem | iccgelb 13385 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄[,]π΅)) β π΄ β€ πΆ) | ||
Theorem | elioo5 13386 | Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β (πΆ β (π΄(,)π΅) β (π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | eliooxr 13387 | A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
β’ (π΄ β (π΅(,)πΆ) β (π΅ β β* β§ πΆ β β*)) | ||
Theorem | eliooord 13388 | Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.) |
β’ (π΄ β (π΅(,)πΆ) β (π΅ < π΄ β§ π΄ < πΆ)) | ||
Theorem | elioo4g 13389 | Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΆ β (π΄(,)π΅) β ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β§ (π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | ioossre 13390 | An open interval is a set of reals. (Contributed by NM, 31-May-2007.) |
β’ (π΄(,)π΅) β β | ||
Theorem | ioosscn 13391 | An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄(,)π΅) β β | ||
Theorem | elioc2 13392 | Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
β’ ((π΄ β β* β§ π΅ β β) β (πΆ β (π΄(,]π΅) β (πΆ β β β§ π΄ < πΆ β§ πΆ β€ π΅))) | ||
Theorem | elico2 13393 | Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β*) β (πΆ β (π΄[,)π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ < π΅))) | ||
Theorem | elicc2 13394 | Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (πΆ β (π΄[,]π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ β€ π΅))) | ||
Theorem | elicc2i 13395 | Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ π΄ β β & β’ π΅ β β β β’ (πΆ β (π΄[,]π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ β€ π΅)) | ||
Theorem | elicc4 13396 | Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β (πΆ β (π΄[,]π΅) β (π΄ β€ πΆ β§ πΆ β€ π΅))) | ||
Theorem | iccss 13397 | Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.) |
β’ (((π΄ β β β§ π΅ β β) β§ (π΄ β€ πΆ β§ π· β€ π΅)) β (πΆ[,]π·) β (π΄[,]π΅)) | ||
Theorem | iccssioo 13398 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ < πΆ β§ π· < π΅)) β (πΆ[,]π·) β (π΄(,)π΅)) | ||
Theorem | icossico 13399 | Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ β€ πΆ β§ π· β€ π΅)) β (πΆ[,)π·) β (π΄[,)π΅)) | ||
Theorem | iccss2 13400 | Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ ((πΆ β (π΄[,]π΅) β§ π· β (π΄[,]π΅)) β (πΆ[,]π·) β (π΄[,]π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |