Type  Label  Description 
Statement 

Theorem  xrleid 9201 
'Less than or equal to' is reflexive for extended reals. (Contributed by
NM, 7Feb2007.)



Theorem  xrletri3 9202 
Trichotomy law for extended reals. (Contributed by FL, 2Aug2009.)



Theorem  xrlelttr 9203 
Transitive law for ordering on extended reals. (Contributed by NM,
19Jan2006.)



Theorem  xrltletr 9204 
Transitive law for ordering on extended reals. (Contributed by NM,
19Jan2006.)



Theorem  xrletr 9205 
Transitive law for ordering on extended reals. (Contributed by NM,
9Feb2006.)



Theorem  xrlttrd 9206 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrlelttrd 9207 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrltletrd 9208 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrletrd 9209 
Transitive law for ordering on extended reals. (Contributed by Mario
Carneiro, 23Aug2015.)



Theorem  xrltne 9210 
'Less than' implies not equal for extended reals. (Contributed by NM,
20Jan2006.)



Theorem  nltpnft 9211 
An extended real is not less than plus infinity iff they are equal.
(Contributed by NM, 30Jan2006.)



Theorem  ngtmnft 9212 
An extended real is not greater than minus infinity iff they are equal.
(Contributed by NM, 2Feb2006.)



Theorem  xrrebnd 9213 
An extended real is real iff it is strictly bounded by infinities.
(Contributed by NM, 2Feb2006.)



Theorem  xrre 9214 
A way of proving that an extended real is real. (Contributed by NM,
9Mar2006.)



Theorem  xrre2 9215 
An extended real between two others is real. (Contributed by NM,
6Feb2007.)



Theorem  xrre3 9216 
A way of proving that an extended real is real. (Contributed by FL,
29May2014.)



Theorem  ge0gtmnf 9217 
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  ge0nemnf 9218 
A nonnegative extended real is greater than negative infinity.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xrrege0 9219 
A nonnegative extended real that is less than a real bound is real.
(Contributed by Mario Carneiro, 20Aug2015.)



Theorem  z2ge 9220* 
There exists an integer greater than or equal to any two others.
(Contributed by NM, 28Aug2005.)



Theorem  xnegeq 9221 
Equality of two extended numbers with in front of them.
(Contributed by FL, 26Dec2011.) (Proof shortened by Mario Carneiro,
20Aug2015.)



Theorem  xnegpnf 9222 
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26Dec2011.)



Theorem  xnegmnf 9223 
Minus . Remark
of [BourbakiTop1] p. IV.15. (Contributed
by FL,
26Dec2011.) (Revised by Mario Carneiro, 20Aug2015.)



Theorem  rexneg 9224 
Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by
FL, 26Dec2011.) (Proof shortened by Mario Carneiro, 20Aug2015.)



Theorem  xneg0 9225 
The negative of zero. (Contributed by Mario Carneiro, 20Aug2015.)



Theorem  xnegcl 9226 
Closure of extended real negative. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xnegneg 9227 
Extended real version of negneg 7676. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xneg11 9228 
Extended real version of neg11 7677. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xltnegi 9229 
Forward direction of xltneg 9230. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xltneg 9230 
Extended real version of ltneg 7884. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xleneg 9231 
Extended real version of leneg 7887. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xlt0neg1 9232 
Extended real version of lt0neg1 7890. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xlt0neg2 9233 
Extended real version of lt0neg2 7891. (Contributed by Mario Carneiro,
20Aug2015.)



Theorem  xle0neg1 9234 
Extended real version of le0neg1 7892. (Contributed by Mario Carneiro,
9Sep2015.)



Theorem  xle0neg2 9235 
Extended real version of le0neg2 7893. (Contributed by Mario Carneiro,
9Sep2015.)



Theorem  xnegcld 9236 
Closure of extended real negative. (Contributed by Mario Carneiro,
28May2016.)



Theorem  xrex 9237 
The set of extended reals exists. (Contributed by NM, 24Dec2006.)



3.5.3 Real number intervals


Syntax  cioo 9238 
Extend class notation with the set of open intervals of extended reals.



Syntax  cioc 9239 
Extend class notation with the set of openbelow, closedabove intervals
of extended reals.



Syntax  cico 9240 
Extend class notation with the set of closedbelow, openabove intervals
of extended reals.



Syntax  cicc 9241 
Extend class notation with the set of closed intervals of extended
reals.



Definition  dfioo 9242* 
Define the set of open intervals of extended reals. (Contributed by NM,
24Dec2006.)



Definition  dfioc 9243* 
Define the set of openbelow, closedabove intervals of extended reals.
(Contributed by NM, 24Dec2006.)



Definition  dfico 9244* 
Define the set of closedbelow, openabove intervals of extended reals.
(Contributed by NM, 24Dec2006.)



Definition  dficc 9245* 
Define the set of closed intervals of extended reals. (Contributed by
NM, 24Dec2006.)



Theorem  ixxval 9246* 
Value of the interval function. (Contributed by Mario Carneiro,
3Nov2013.)



Theorem  elixx1 9247* 
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3Nov2013.)



Theorem  ixxf 9248* 
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by FL, 14Jun2007.) (Revised by Mario Carneiro,
16Nov2013.)



Theorem  ixxex 9249* 
The set of intervals of extended reals exists. (Contributed by Mario
Carneiro, 3Nov2013.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  ixxssxr 9250* 
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4Jul2014.)



Theorem  elixx3g 9251* 
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,
3Nov2013.)



Theorem  ixxssixx 9252* 
An interval is a subset of its closure. (Contributed by Paul Chapman,
18Oct2007.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  ixxdisj 9253* 
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16Jun2014.)



Theorem  ixxss1 9254* 
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3Nov2013.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  ixxss2 9255* 
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3Nov2013.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  ixxss12 9256* 
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20Feb2015.) (Revised by Mario Carneiro,
28Apr2015.)



Theorem  iooex 9257 
The set of open intervals of extended reals exists. (Contributed by NM,
6Feb2007.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iooval 9258* 
Value of the open interval function. (Contributed by NM, 24Dec2006.)
(Revised by Mario Carneiro, 3Nov2013.)



Theorem  iooidg 9259 
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29Mar2020.)



Theorem  elioo3g 9260 
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, 24Dec2006.)
(Revised by Mario Carneiro, 3Nov2013.)



Theorem  elioo1 9261 
Membership in an open interval of extended reals. (Contributed by NM,
24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  elioore 9262 
A member of an open interval of reals is a real. (Contributed by NM,
17Aug2008.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  lbioog 9263 
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30Mar2020.)



Theorem  ubioog 9264 
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30Mar2020.)



Theorem  iooval2 9265* 
Value of the open interval function. (Contributed by NM, 6Feb2007.)
(Revised by Mario Carneiro, 3Nov2013.)



Theorem  iooss1 9266 
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7Feb2007.) (Revised by Mario Carneiro, 20Feb2015.)



Theorem  iooss2 9267 
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7Feb2007.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iocval 9268* 
Value of the openbelow, closedabove interval function. (Contributed
by NM, 24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  icoval 9269* 
Value of the closedbelow, openabove interval function. (Contributed
by NM, 24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iccval 9270* 
Value of the closed interval function. (Contributed by NM,
24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  elioo2 9271 
Membership in an open interval of extended reals. (Contributed by NM,
6Feb2007.)



Theorem  elioc1 9272 
Membership in an openbelow, closedabove interval of extended reals.
(Contributed by NM, 24Dec2006.) (Revised by Mario Carneiro,
3Nov2013.)



Theorem  elico1 9273 
Membership in a closedbelow, openabove interval of extended reals.
(Contributed by NM, 24Dec2006.) (Revised by Mario Carneiro,
3Nov2013.)



Theorem  elicc1 9274 
Membership in a closed interval of extended reals. (Contributed by NM,
24Dec2006.) (Revised by Mario Carneiro, 3Nov2013.)



Theorem  iccid 9275 
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13Jul2009.)



Theorem  icc0r 9276 
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30Mar2020.)



Theorem  eliooxr 9277 
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17Aug2008.)



Theorem  eliooord 9278 
Ordering implied by a member of an open interval of reals. (Contributed
by NM, 17Aug2008.) (Revised by Mario Carneiro, 9May2014.)



Theorem  ubioc1 9279 
The upper bound belongs to an openbelow, closedabove interval. See
ubicc2 9334. (Contributed by FL, 29May2014.)



Theorem  lbico1 9280 
The lower bound belongs to a closedbelow, openabove interval. See
lbicc2 9333. (Contributed by FL, 29May2014.)



Theorem  iccleub 9281 
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14Jul2009.)



Theorem  iccgelb 9282 
An element of a closed interval is more than or equal to its lower bound
(Contributed by Thierry Arnoux, 23Dec2016.)



Theorem  elioo5 9283 
Membership in an open interval of extended reals. (Contributed by NM,
17Aug2008.)



Theorem  elioo4g 9284 
Membership in an open interval of extended reals. (Contributed by NM,
8Jun2007.) (Revised by Mario Carneiro, 28Apr2015.)



Theorem  ioossre 9285 
An open interval is a set of reals. (Contributed by NM,
31May2007.)



Theorem  elioc2 9286 
Membership in an openbelow, closedabove real interval. (Contributed by
Paul Chapman, 30Dec2007.) (Revised by Mario Carneiro, 14Jun2014.)



Theorem  elico2 9287 
Membership in a closedbelow, openabove real interval. (Contributed by
Paul Chapman, 21Jan2008.) (Revised by Mario Carneiro, 14Jun2014.)



Theorem  elicc2 9288 
Membership in a closed real interval. (Contributed by Paul Chapman,
21Sep2007.) (Revised by Mario Carneiro, 14Jun2014.)



Theorem  elicc2i 9289 
Inference for membership in a closed interval. (Contributed by Scott
Fenton, 3Jun2013.)



Theorem  elicc4 9290 
Membership in a closed real interval. (Contributed by Stefan O'Rear,
16Nov2014.) (Proof shortened by Mario Carneiro, 1Jan2017.)



Theorem  iccss 9291 
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2Sep2009.) (Revised by Mario
Carneiro, 20Feb2015.)



Theorem  iccssioo 9292 
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20Feb2015.)



Theorem  icossico 9293 
Condition for a closedbelow, openabove interval to be a subset of a
closedbelow, openabove interval. (Contributed by Thierry Arnoux,
21Sep2017.)



Theorem  iccss2 9294 
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2Sep2009.) (Revised by Mario
Carneiro, 28Apr2015.)



Theorem  iccssico 9295 
Condition for a closed interval to be a subset of a halfopen interval.
(Contributed by Mario Carneiro, 9Sep2015.)



Theorem  iccssioo2 9296 
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20Feb2015.)



Theorem  iccssico2 9297 
Condition for a closed interval to be a subset of a closedbelow,
openabove interval. (Contributed by Mario Carneiro, 20Feb2015.)



Theorem  ioomax 9298 
The open interval from minus to plus infinity. (Contributed by NM,
6Feb2007.)



Theorem  iccmax 9299 
The closed interval from minus to plus infinity. (Contributed by Mario
Carneiro, 4Jul2014.)



Theorem  ioopos 9300 
The set of positive reals expressed as an open interval. (Contributed by
NM, 7May2007.)

