![]() |
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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | supxrunb2 13301* | The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ < π¦ β sup(π΄, β*, < ) = +β)) | ||
Theorem | supxrbnd1 13302* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ < π₯ β sup(π΄, β*, < ) < +β)) | ||
Theorem | supxrbnd2 13303* | The supremum of a bounded-above set of extended reals is less than infinity. (Contributed by NM, 30-Jan-2006.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ β€ π₯ β sup(π΄, β*, < ) < +β)) | ||
Theorem | xrsup0 13304 | The supremum of an empty set under the extended reals is minus infinity. (Contributed by NM, 15-Oct-2005.) |
β’ sup(β , β*, < ) = -β | ||
Theorem | supxrub 13305 | 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 13306* | 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 13307* | 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 13308* | 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 13309 | The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.) |
β’ ((π΄ β β β§ π΄ β β β§ sup(π΄, β*, < ) < +β) β sup(π΄, β*, < ) β β) | ||
Theorem | supxrgtmnf 13310 | The supremum of a nonempty set of reals is greater than minus infinity. (Contributed by NM, 2-Feb-2006.) |
β’ ((π΄ β β β§ π΄ β β ) β -β < sup(π΄, β*, < )) | ||
Theorem | supxrre1 13311 | 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 13312 | 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 13313 | Smaller sets of extended reals have smaller suprema. (Contributed by Mario Carneiro, 1-Apr-2015.) |
β’ ((π΄ β π΅ β§ π΅ β β*) β sup(π΄, β*, < ) β€ sup(π΅, β*, < )) | ||
Theorem | infxrcl 13314 | 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 13315 | 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 13316* | 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 13317* | 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 13318 | 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 13319 | 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 13320 | 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 13321* | For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β βπ¦ β β π¦ < π₯ | ||
Theorem | rpltrp 13322* | For all positive real numbers there is a smaller positive real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β+ βπ¦ β β+ π¦ < π₯ | ||
Theorem | reltxrnmnf 13323* | For all extended real numbers not being minus infinity there is a smaller real number. (Contributed by AV, 5-Sep-2020.) |
β’ βπ₯ β β* (-β < π₯ β βπ¦ β β π¦ < π₯) | ||
Theorem | infmremnf 13324 | The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020.) |
β’ inf(β, β*, < ) = -β | ||
Theorem | infmrp1 13325 | The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020.) |
β’ inf(β+, β, < ) = 0 | ||
Syntax | cioo 13326 | Extend class notation with the set of open intervals of extended reals. |
class (,) | ||
Syntax | cioc 13327 | Extend class notation with the set of open-below, closed-above intervals of extended reals. |
class (,] | ||
Syntax | cico 13328 | Extend class notation with the set of closed-below, open-above intervals of extended reals. |
class [,) | ||
Syntax | cicc 13329 | Extend class notation with the set of closed intervals of extended reals. |
class [,] | ||
Definition | df-ioo 13330* | Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ (,) = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) | ||
Definition | df-ioc 13331* | Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ (,] = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ β€ π¦)}) | ||
Definition | df-ico 13332* | Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ [,) = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π¦)}) | ||
Definition | df-icc 13333* | Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.) |
β’ [,] = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ β€ π¦)}) | ||
Theorem | ixxval 13334* | Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ ((π΄ β β* β§ π΅ β β*) β (π΄ππ΅) = {π§ β β* β£ (π΄π π§ β§ π§ππ΅)}) | ||
Theorem | elixx1 13335* | Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄ππ΅) β (πΆ β β* β§ π΄π πΆ β§ πΆππ΅))) | ||
Theorem | ixxf 13336* | 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 13337* | 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 13338* | The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) β β’ (π΄ππ΅) β β* | ||
Theorem | elixx3g 13339* | 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 13340* | An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ π€ β β*) β (π΄π π€ β π΄ππ€)) & β’ ((π€ β β* β§ π΅ β β*) β (π€ππ΅ β π€ππ΅)) β β’ (π΄ππ΅) β (π΄ππ΅) | ||
Theorem | ixxdisj 13341* | Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΅ β β* β§ π€ β β*) β (π΅ππ€ β Β¬ π€ππ΅)) β β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β ((π΄ππ΅) β© (π΅ππΆ)) = β ) | ||
Theorem | ixxun 13342* | Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΅ β β* β§ π€ β β*) β (π΅ππ€ β Β¬ π€ππ΅)) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β* β§ πΆ β β*) β ((π€ππ΅ β§ π΅ππΆ) β π€ππΆ)) & β’ ((π΄ β β* β§ π΅ β β* β§ π€ β β*) β ((π΄ππ΅ β§ π΅ππ€) β π΄π π€)) β β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ππ΅ β§ π΅ππΆ)) β ((π΄ππ΅) βͺ (π΅ππΆ)) = (π΄ππΆ)) | ||
Theorem | ixxin 13343* | Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ πΆ β β* β§ π§ β β*) β (if(π΄ β€ πΆ, πΆ, π΄)π π§ β (π΄π π§ β§ πΆπ π§))) & β’ ((π§ β β* β§ π΅ β β* β§ π· β β*) β (π§πif(π΅ β€ π·, π΅, π·) β (π§ππ΅ β§ π§ππ·))) β β’ (((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β ((π΄ππ΅) β© (πΆππ·)) = (if(π΄ β€ πΆ, πΆ, π΄)πif(π΅ β€ π·, π΅, π·))) | ||
Theorem | ixxss1 13344* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ π΅ β β* β§ π€ β β*) β ((π΄ππ΅ β§ π΅ππ€) β π΄π π€)) β β’ ((π΄ β β* β§ π΄ππ΅) β (π΅ππΆ) β (π΄ππΆ)) | ||
Theorem | ixxss2 13345* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β* β§ πΆ β β*) β ((π€ππ΅ β§ π΅ππΆ) β π€ππΆ)) β β’ ((πΆ β β* β§ π΅ππΆ) β (π΄ππ΅) β (π΄ππΆ)) | ||
Theorem | ixxss12 13346* | Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β* β§ πΆ β β* β§ π€ β β*) β ((π΄ππΆ β§ πΆππ€) β π΄π π€)) & β’ ((π€ β β* β§ π· β β* β§ π΅ β β*) β ((π€ππ· β§ π·ππ΅) β π€ππ΅)) β β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ππΆ β§ π·ππ΅)) β (πΆππ·) β (π΄ππ΅)) | ||
Theorem | ixxub 13347* | Extract the upper bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β*) β (π€ < π΅ β π€ππ΅)) & β’ ((π€ β β* β§ π΅ β β*) β (π€ππ΅ β π€ β€ π΅)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄ < π€ β π΄π π€)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄π π€ β π΄ β€ π€)) β β’ ((π΄ β β* β§ π΅ β β* β§ (π΄ππ΅) β β ) β sup((π΄ππ΅), β*, < ) = π΅) | ||
Theorem | ixxlb 13348* | Extract the lower bound of an interval. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by AV, 12-Sep-2020.) |
β’ π = (π₯ β β*, π¦ β β* β¦ {π§ β β* β£ (π₯π π§ β§ π§ππ¦)}) & β’ ((π€ β β* β§ π΅ β β*) β (π€ < π΅ β π€ππ΅)) & β’ ((π€ β β* β§ π΅ β β*) β (π€ππ΅ β π€ β€ π΅)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄ < π€ β π΄π π€)) & β’ ((π΄ β β* β§ π€ β β*) β (π΄π π€ β π΄ β€ π€)) β β’ ((π΄ β β* β§ π΅ β β* β§ (π΄ππ΅) β β ) β inf((π΄ππ΅), β*, < ) = π΄) | ||
Theorem | iooex 13349 | 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 13350* | Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄(,)π΅) = {π₯ β β* β£ (π΄ < π₯ β§ π₯ < π΅)}) | ||
Theorem | ioo0 13351 | An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄(,)π΅) = β β π΅ β€ π΄)) | ||
Theorem | ioon0 13352 | 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 13353 | 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 13354 | 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 13355 | 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 13356 | 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 13357 | An open interval does not contain its left endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ Β¬ π΄ β (π΄(,)π΅) | ||
Theorem | ubioo 13358 | An open interval does not contain its right endpoint. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ Β¬ π΅ β (π΄(,)π΅) | ||
Theorem | iooval2 13359* | Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄(,)π΅) = {π₯ β β β£ (π΄ < π₯ β§ π₯ < π΅)}) | ||
Theorem | iooin 13360 | 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 13361 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.) |
β’ ((π΄ β β* β§ π΄ β€ π΅) β (π΅(,)πΆ) β (π΄(,)πΆ)) | ||
Theorem | iooss2 13362 | Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((πΆ β β* β§ π΅ β€ πΆ) β (π΄(,)π΅) β (π΄(,)πΆ)) | ||
Theorem | iocval 13363* | Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄(,]π΅) = {π₯ β β* β£ (π΄ < π₯ β§ π₯ β€ π΅)}) | ||
Theorem | icoval 13364* | Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ < π΅)}) | ||
Theorem | iccval 13365* | Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄[,]π΅) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ β€ π΅)}) | ||
Theorem | elioo1 13366 | Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄(,)π΅) β (πΆ β β* β§ π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | elioo2 13367 | Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄(,)π΅) β (πΆ β β β§ π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | elioc1 13368 | 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 13369 | 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 13370 | Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π΄ β β* β§ π΅ β β*) β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ πΆ β§ πΆ β€ π΅))) | ||
Theorem | iccid 13371 | A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.) |
β’ (π΄ β β* β (π΄[,]π΄) = {π΄}) | ||
Theorem | ico0 13372 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄[,)π΅) = β β π΅ β€ π΄)) | ||
Theorem | ioc0 13373 | An empty open interval of extended reals. (Contributed by FL, 30-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄(,]π΅) = β β π΅ β€ π΄)) | ||
Theorem | icc0 13374 | An empty closed interval of extended reals. (Contributed by FL, 30-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄[,]π΅) = β β π΅ < π΄)) | ||
Theorem | dfrp2 13375 | Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020.) |
β’ β+ = (0(,)+β) | ||
Theorem | elicod 13376 | Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ πΆ) & β’ (π β πΆ < π΅) β β’ (π β πΆ β (π΄[,)π΅)) | ||
Theorem | icogelb 13377 | 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 13378 | A member of a left-closed right-open interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ πΆ β (π΄[,)π΅)) β πΆ β β) | ||
Theorem | ubioc1 13379 | The upper bound belongs to an open-below, closed-above interval. See ubicc2 13444. (Contributed by FL, 29-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β π΅ β (π΄(,]π΅)) | ||
Theorem | lbico1 13380 | The lower bound belongs to a closed-below, open-above interval. See lbicc2 13443. (Contributed by FL, 29-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β π΄ β (π΄[,)π΅)) | ||
Theorem | iccleub 13381 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄[,]π΅)) β πΆ β€ π΅) | ||
Theorem | iccgelb 13382 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Thierry Arnoux, 23-Dec-2016.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄[,]π΅)) β π΄ β€ πΆ) | ||
Theorem | elioo5 13383 | Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β (πΆ β (π΄(,)π΅) β (π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | eliooxr 13384 | A nonempty open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.) |
β’ (π΄ β (π΅(,)πΆ) β (π΅ β β* β§ πΆ β β*)) | ||
Theorem | eliooord 13385 | 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 13386 | Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΆ β (π΄(,)π΅) β ((π΄ β β* β§ π΅ β β* β§ πΆ β β) β§ (π΄ < πΆ β§ πΆ < π΅))) | ||
Theorem | ioossre 13387 | An open interval is a set of reals. (Contributed by NM, 31-May-2007.) |
β’ (π΄(,)π΅) β β | ||
Theorem | ioosscn 13388 | An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄(,)π΅) β β | ||
Theorem | elioc2 13389 | 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 13390 | 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 13391 | Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (πΆ β (π΄[,]π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ β€ π΅))) | ||
Theorem | elicc2i 13392 | Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.) |
β’ π΄ β β & β’ π΅ β β β β’ (πΆ β (π΄[,]π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ β€ π΅)) | ||
Theorem | elicc4 13393 | Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β (πΆ β (π΄[,]π΅) β (π΄ β€ πΆ β§ πΆ β€ π΅))) | ||
Theorem | iccss 13394 | 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 13395 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ < πΆ β§ π· < π΅)) β (πΆ[,]π·) β (π΄(,)π΅)) | ||
Theorem | icossico 13396 | 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 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, 28-Apr-2015.) |
β’ ((πΆ β (π΄[,]π΅) β§ π· β (π΄[,]π΅)) β (πΆ[,]π·) β (π΄[,]π΅)) | ||
Theorem | iccssico 13398 | Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ β€ πΆ β§ π· < π΅)) β (πΆ[,]π·) β (π΄[,)π΅)) | ||
Theorem | iccssioo2 13399 | Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
β’ ((πΆ β (π΄(,)π΅) β§ π· β (π΄(,)π΅)) β (πΆ[,]π·) β (π΄(,)π΅)) | ||
Theorem | iccssico2 13400 | Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.) |
β’ ((πΆ β (π΄[,)π΅) β§ π· β (π΄[,)π΅)) β (πΆ[,]π·) β (π΄[,)π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |