:: Basic Properties of Extended Real Numbers :: by Andrzej Trybulec, Yatsuka Nakamura, Artur Korni{\l}owicz and :: Adam Grabowski :: :: Received January 22, 2007 :: Copyright (c) 2007-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XXREAL_0, SUBSET_1, NUMBERS, MEMBERED, XBOOLE_0, ARYTM_3, TARSKI, REAL_1, XXREAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XREAL_0; constructors NUMBERS, XXREAL_0, XREAL_0, MEMBERED; registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED; requirements SUBSET, BOOLE; begin reserve x for set, p,q,r,s,t,u for ExtReal, g for Real, a for Element of ExtREAL; scheme :: XXREAL_1:sch 1 Conti { P,Q[object] }: ex s st (for r st P[r] holds r <= s) & for r st Q[r] holds s <= r provided for r,s st P[r] & Q[s] holds r <= s; begin :: Intervals definition let r,s be ExtReal; func [.r,s.] -> set equals :: XXREAL_1:def 1 { a : r <= a & a <= s }; func [.r,s.[ -> set equals :: XXREAL_1:def 2 { a : r <= a & a < s }; func ].r,s.] -> set equals :: XXREAL_1:def 3 { a : r < a & a <= s }; func ].r,s.[ -> set equals :: XXREAL_1:def 4 { a : r < a & a < s }; end; theorem :: XXREAL_1:1 t in [.r,s.] iff r <= t & t <= s; theorem :: XXREAL_1:2 t in ].r,s.] iff r < t & t <= s; theorem :: XXREAL_1:3 t in [.r,s.[ iff r <= t & t < s; theorem :: XXREAL_1:4 t in ].r,s.[ iff r < t & t < s; registration let r,s; :: MEASURE5:11 cluster [.r,s.] -> ext-real-membered; cluster [.r,s.[ -> ext-real-membered; cluster ].r,s.] -> ext-real-membered; cluster ].r,s.[ -> ext-real-membered; end; theorem :: XXREAL_1:5 x in [.p,q.] implies x in ].p,q.[ or x = p or x = q; theorem :: XXREAL_1:6 x in [.p,q.] implies x in ].p,q.] or x = p; theorem :: XXREAL_1:7 x in [.p,q.] implies x in [.p,q.[ or x = q; theorem :: XXREAL_1:8 x in [.p,q.[ implies x in ].p,q.[ or x = p; theorem :: XXREAL_1:9 x in ].p,q.] implies x in ].p,q.[ or x = q; theorem :: XXREAL_1:10 x in [.p,q.[ implies x in ].p,q.] & x <> q or x = p; theorem :: XXREAL_1:11 x in ].p,q.] implies x in [.p,q.[ & x <> p or x = q; theorem :: XXREAL_1:12 x in ].p,q.] implies x in [.p,q.] & x <> p; theorem :: XXREAL_1:13 x in [.p,q.[ implies x in [.p,q.] & x <> q; theorem :: XXREAL_1:14 x in ].p,q.[ implies x in [.p,q.[ & x <> p; theorem :: XXREAL_1:15 x in ].p,q.[ implies x in ].p,q.] & x <> q; theorem :: XXREAL_1:16 x in ].p,q.[ implies x in [.p,q.] & x <> p & x <> q; theorem :: XXREAL_1:17 :: MEASURE5:14 [.r,r.] = {r}; theorem :: XXREAL_1:18 :: MEASURE5:13 [.r,r.[ = {}; theorem :: XXREAL_1:19 :: MEASURE5:13 ].r,r.] = {}; theorem :: XXREAL_1:20 :: MEASURE5:13 ].r,r.[ = {}; registration let r; cluster [.r,r.] -> non empty; cluster [.r,r.[ -> empty; cluster ].r,r.] -> empty; cluster ].r,r.[ -> empty; end; theorem :: XXREAL_1:21 ].p,q.[ c= ].p,q.]; theorem :: XXREAL_1:22 ].p,q.[ c= [.p,q.[; theorem :: XXREAL_1:23 ].p,q.] c= [.p,q.]; theorem :: XXREAL_1:24 [.p,q.[ c= [.p,q.]; theorem :: XXREAL_1:25 ].p,q.[ c= [.p,q.]; theorem :: XXREAL_1:26 :: MEASURE5:12,15 p <= q implies ].q,p.] = {}; theorem :: XXREAL_1:27 :: MEASURE5:12,15 p <= q implies [.q,p.[ = {}; theorem :: XXREAL_1:28 :: MEASURE5:12,15 p <= q implies ].q,p.[ = {}; theorem :: XXREAL_1:29 :: MEASURE5:12 p < q implies [.q,p.] = {}; theorem :: XXREAL_1:30 r <= s implies [.r,s.] is non empty; theorem :: XXREAL_1:31 p < q implies [.p,q.[ is non empty; theorem :: XXREAL_1:32 p < q implies ].p,q.] is non empty; theorem :: XXREAL_1:33 p < q implies ].p,q.[ is non empty; theorem :: XXREAL_1:34 p <= r & s <= q implies [.r,s.] c= [.p,q.]; theorem :: XXREAL_1:35 p <= r & s <= q implies [.r,s.[ c= [.p,q.]; theorem :: XXREAL_1:36 p <= r & s <= q implies ].r,s.] c= [.p,q.]; theorem :: XXREAL_1:37 p <= r & s <= q implies ].r,s.[ c= [.p,q.]; theorem :: XXREAL_1:38 p <= r & s <= q implies [.r,s.[ c= [.p,q.[; theorem :: XXREAL_1:39 p < r & s <= q implies [.r,s.] c= ].p,q.]; theorem :: XXREAL_1:40 p < r & s <= q implies [.r,s.[ c= ].p,q.]; theorem :: XXREAL_1:41 p <= r & s <= q implies ].r,s.[ c= ].p,q.]; theorem :: XXREAL_1:42 p <= r & s <= q implies ].r,s.] c= ].p,q.]; theorem :: XXREAL_1:43 p <= r & s < q implies [.r,s.] c= [.p,q.[; theorem :: XXREAL_1:44 p <= r & s < q implies ].r,s.] c= [.p,q.[; theorem :: XXREAL_1:45 p <= r & s <= q implies ].r,s.[ c= [.p,q.[; theorem :: XXREAL_1:46 p <= r & s <= q implies ].r,s.[ c= ].p,q.[; theorem :: XXREAL_1:47 p < r & s < q implies [.r,s.] c= ].p,q.[; theorem :: XXREAL_1:48 p < r & s <= q implies [.r,s.[ c= ].p,q.[; theorem :: XXREAL_1:49 p <= r & s < q implies ].r,s.] c= ].p,q.[; theorem :: XXREAL_1:50 r <= s & [.r,s.] c= [.p,q.] implies p <= r & s <= q; theorem :: XXREAL_1:51 r < s & ].r,s.[ c= [.p,q.] implies p <= r & s <= q; theorem :: XXREAL_1:52 r < s & [.r,s.[ c= [.p,q.] implies p <= r & s <= q; theorem :: XXREAL_1:53 r < s & ].r,s.] c= [.p,q.] implies p <= r & s <= q; theorem :: XXREAL_1:54 r <= s & [.r,s.] c= [.p,q.[ implies p <= r & s < q; theorem :: XXREAL_1:55 r < s & [.r,s.[ c= [.p,q.[ implies p <= r & s <= q; theorem :: XXREAL_1:56 r < s & ].r,s.[ c= [.p,q.[ implies p <= r & s <= q; theorem :: XXREAL_1:57 r < s & ].r,s.] c= [.p,q.[ implies p <= r & s < q; theorem :: XXREAL_1:58 r <= s & [.r,s.] c= ].p,q.] implies p < r & s <= q; theorem :: XXREAL_1:59 r < s & ].r,s.[ c= ].p,q.] implies p <= r & s <= q; theorem :: XXREAL_1:60 r < s & [.r,s.[ c= ].p,q.] implies p < r & s <= q; theorem :: XXREAL_1:61 r < s & ].r,s.] c= ].p,q.] implies p <= r & s <= q; theorem :: XXREAL_1:62 r <= s & [.r,s.] c= ].p,q.[ implies p < r & s < q; theorem :: XXREAL_1:63 r < s & ].r,s.[ c= ].p,q.[ implies p <= r & s <= q; theorem :: XXREAL_1:64 r < s & [.r,s.[ c= ].p,q.[ implies p < r & s <= q; theorem :: XXREAL_1:65 r < s & ].r,s.] c= ].p,q.[ implies p <= r & s < q; theorem :: XXREAL_1:66 :: INTEGRA1:6 ?? p <= q & [.p,q.] = [.r,s.] implies p = r & q = s; theorem :: XXREAL_1:67 p < q & ].p,q.[ = ].r,s.[ implies p = r & q = s; theorem :: XXREAL_1:68 p < q & ].p,q.] = ].r,s.] implies p = r & q = s; theorem :: XXREAL_1:69 p < q & [.p,q.[ = [.r,s.[ implies p = r & q = s; theorem :: XXREAL_1:70 r <= s implies [.r,s.] <> ].p,q.]; theorem :: XXREAL_1:71 r <= s implies [.r,s.] <> [.p,q.[; theorem :: XXREAL_1:72 r <= s implies [.r,s.] <> ].p,q.[; theorem :: XXREAL_1:73 r < s implies [.r,s.[ <> [.p,q.]; theorem :: XXREAL_1:74 r < s implies [.r,s.[ <> ].p,q.]; theorem :: XXREAL_1:75 r < s implies [.r,s.[ <> ].p,q.[; theorem :: XXREAL_1:76 r < s implies ].r,s.] <> [.p,q.]; theorem :: XXREAL_1:77 r < s implies ].r,s.] <> [.p,q.[; theorem :: XXREAL_1:78 r < s implies ].r,s.] <> ].p,q.[; theorem :: XXREAL_1:79 r < s implies ].r,s.[ <> [.p,q.]; theorem :: XXREAL_1:80 r < s implies ].r,s.[ <> ].p,q.]; theorem :: XXREAL_1:81 r < s implies ].r,s.[ <> [.p,q.[; theorem :: XXREAL_1:82 r <= s & [.r,s.] c< [.p,q.] implies p < r or s < q; theorem :: XXREAL_1:83 r < s & ].r,s.[ c= [.p,q.] implies [.r,s.] c= [.p,q.]; theorem :: XXREAL_1:84 r < s implies [.s,p.[ c= ].r,p.[; theorem :: XXREAL_1:85 :: MEASURE5:15 s <= r implies [.r,s.] c= {r} & [.r,s.] c= {s}; theorem :: XXREAL_1:86 ].r,s.[ misses {r,s}; theorem :: XXREAL_1:87 [.r,s.[ misses {s}; theorem :: XXREAL_1:88 ].r,s.] misses {r}; theorem :: XXREAL_1:89 s <= p implies [.r,s.] misses ].p,q.[; theorem :: XXREAL_1:90 s <= p implies [.r,s.] misses ].p,q.]; theorem :: XXREAL_1:91 s <= p implies ].r,s.] misses ].p,q.[; theorem :: XXREAL_1:92 s <= p implies ].r,s.] misses ].p,q.]; theorem :: XXREAL_1:93 s <= p implies ].r,s.[ misses [.p,q.]; theorem :: XXREAL_1:94 s <= p implies ].r,s.[ misses [.p,q.[; theorem :: XXREAL_1:95 s <= p implies [.r,s.[ misses [.p,q.]; theorem :: XXREAL_1:96 s <= p implies [.r,s.[ misses [.p,q.[; theorem :: XXREAL_1:97 :: MEASURE5:24 r < p & r < s implies not ].r,s.[ c= [.p,q.]; theorem :: XXREAL_1:98 :: MEASURE5:38 r < p & r < s implies not [.r,s.[ c= [.p,q.]; theorem :: XXREAL_1:99 :: MEASURE5:42 r < p & r < s implies not ].r,s.] c= [.p,q.]; theorem :: XXREAL_1:100 :: MEASURE5:34 r < p & r <= s implies not [.r,s.] c= [.p,q.]; theorem :: XXREAL_1:101 :: MEASURE5:26 r < p & r < s implies not ].r,s.[ c= [.p,q.[; theorem :: XXREAL_1:102 :: MEASURE5:48 r < p & r < s implies not ].r,s.] c= [.p,q.[; theorem :: XXREAL_1:103 r < p & r < s implies not [.r,s.[ c= [.p,q.[; theorem :: XXREAL_1:104 :: MEASURE5:44 r < p & r <= s implies not [.r,s.] c= [.p,q.[; theorem :: XXREAL_1:105 :: MEASURE5:30 r < p & r < s implies not ].r,s.[ c= ].p,q.]; theorem :: XXREAL_1:106 :: MEASURE5:46 r <= p & r < s implies not [.r,s.[ c= ].p,q.]; theorem :: XXREAL_1:107 :: MEASURE5:50 r < p & r < s implies not ].r,s.] c= ].p,q.]; theorem :: XXREAL_1:108 :: MEASURE5:40 r <= p & r <= s implies not [.r,s.] c= ].p,q.]; theorem :: XXREAL_1:109 :: MEASURE5:22 :: MEASURE5:36 r <= p & r <= s implies not [.r,s.] c= ].p,q.[; theorem :: XXREAL_1:110 :: MEASURE5:28 r <= p & r < s implies not [.r,s.[ c= ].p,q.[; theorem :: XXREAL_1:111 :: MEASURE5:32 r < p & r < s implies not ].r,s.] c= ].p,q.[; theorem :: XXREAL_1:112 :: MEASURE5:20 r < p & r < s implies not ].r,s.[ c= ].p,q.[; theorem :: XXREAL_1:113 :: MEASURE5:21 q < s & r < s implies not ].r,s.[ c= [.p,q.]; theorem :: XXREAL_1:114 q < s & r < s implies not [.r,s.[ c= [.p,q.]; theorem :: XXREAL_1:115 q < s & r < s implies not ].r,s.] c= [.p,q.]; theorem :: XXREAL_1:116 q < s & r <= s implies not [.r,s.] c= [.p,q.]; theorem :: XXREAL_1:117 q < s & r < s implies not ].r,s.[ c= [.p,q.[; theorem :: XXREAL_1:118 q <= s & r < s implies not ].r,s.] c= [.p,q.[; theorem :: XXREAL_1:119 q < s & r < s implies not [.r,s.[ c= [.p,q.[; theorem :: XXREAL_1:120 q < s & r < s implies not ].r,s.[ c= ].p,q.]; theorem :: XXREAL_1:121 q < s & r <= s implies not [.r,s.] c= ].p,q.]; theorem :: XXREAL_1:122 q < s & r < s implies not [.r,s.[ c= ].p,q.]; theorem :: XXREAL_1:123 q < s & r < s implies not ].r,s.] c= ].p,q.]; theorem :: XXREAL_1:124 q <= s & r <= s implies not [.r,s.] c= ].p,q.[; theorem :: XXREAL_1:125 q < s & r < s implies not [.r,s.[ c= ].p,q.[; theorem :: XXREAL_1:126 q <= s & r < s implies not ].r,s.] c= ].p,q.[; theorem :: XXREAL_1:127 q < s & r < s implies not ].r,s.[ c= ].p,q.[; begin :: Boolean operations theorem :: XXREAL_1:128 r <= s implies [.r,s.] = ].r,s.[ \/ {r,s}; theorem :: XXREAL_1:129 r <= s implies [.r,s.] = [.r,s.[ \/ {s}; theorem :: XXREAL_1:130 r <= s implies [.r,s.] = {r} \/ ].r,s.]; theorem :: XXREAL_1:131 r < s implies [.r,s.[ = {r} \/ ].r,s.[; theorem :: XXREAL_1:132 r < s implies ].r,s.] = ].r,s.[ \/ {s}; theorem :: XXREAL_1:133 r <= s implies [.r,s.] \ {r,s} = ].r,s.[; theorem :: XXREAL_1:134 r <= s implies [.r,s.] \ {r} = ].r,s.]; theorem :: XXREAL_1:135 r <= s implies [.r,s.] \ {s} = [.r,s.[; theorem :: XXREAL_1:136 r < s implies [.r,s.[ \ {r} = ].r,s.[; theorem :: XXREAL_1:137 r < s implies ].r,s.] \ {s} = ].r,s.[; theorem :: XXREAL_1:138 r < s & s < t implies ].r,s.] /\ [.s,t.[ = {s}; theorem :: XXREAL_1:139 [.r,s.[ /\ [.p,q.[ = [.max(r,p),min(s,q).[; theorem :: XXREAL_1:140 [.r,s.] /\ [.p,q.] = [.max(r,p),min(s,q).]; theorem :: XXREAL_1:141 ].r,s.] /\ ].p,q.] = ].max(r,p),min(s,q).]; theorem :: XXREAL_1:142 ].r,s.[ /\ ].p,q.[ = ].max(r,p),min(s,q).[; theorem :: XXREAL_1:143 r <= p & s <= q implies [.r,s.] /\ [.p,q.] = [.p,s.]; theorem :: XXREAL_1:144 r <= p & s <= q implies [.r,s.[ /\ [.p,q.] = [.p,s.[; theorem :: XXREAL_1:145 r >= p & s > q implies [.r,s.[ /\ [.p,q.] = [.r,q.]; theorem :: XXREAL_1:146 r < p & s <= q implies ].r,s.] /\ [.p,q.] = [.p,s.]; theorem :: XXREAL_1:147 r >= p & s >= q implies ].r,s.] /\ [.p,q.] = ].r,q.]; theorem :: XXREAL_1:148 r < p & s <= q implies ].r,s.[ /\ [.p,q.] = [.p,s.[; theorem :: XXREAL_1:149 r >= p & s > q implies ].r,s.[ /\ [.p,q.] = ].r,q.]; theorem :: XXREAL_1:150 r <= p & s <= q implies [.r,s.[ /\ [.p,q.[ = [.p,s.[; theorem :: XXREAL_1:151 r >= p & s >= q implies [.r,s.[ /\ [.p,q.[ = [.r,q.[; theorem :: XXREAL_1:152 r < p & s < q implies ].r,s.] /\ [.p,q.[ = [.p,s.]; theorem :: XXREAL_1:153 r >= p & s >= q implies ].r,s.] /\ [.p,q.[ = ].r,q.[; theorem :: XXREAL_1:154 r < p & s <= q implies ].r,s.[ /\ [.p,q.[ = [.p,s.[; theorem :: XXREAL_1:155 r >= p & s >= q implies ].r,s.[ /\ [.p,q.[ = ].r,q.[; theorem :: XXREAL_1:156 r <= p & s <= q implies ].r,s.] /\ ].p,q.] = ].p,s.]; theorem :: XXREAL_1:157 r >= p & s >= q implies ].r,s.] /\ ].p,q.] = ].r,q.]; theorem :: XXREAL_1:158 r <= p & s <= q implies ].r,s.[ /\ ].p,q.] = ].p,s.[; theorem :: XXREAL_1:159 r >= p & s > q implies ].r,s.[ /\ ].p,q.] = ].r,q.]; theorem :: XXREAL_1:160 r <= p & s <= q implies ].r,s.[ /\ ].p,q.[ = ].p,s.[; theorem :: XXREAL_1:161 [.r,s.[ \/ [.p,q.[ c= [.min(r,p),max(s,q).[; theorem :: XXREAL_1:162 [.r,s.[ meets [.p,q.[ implies [.r,s.[ \/ [.p,q.[ = [.min(r,p),max(s,q).[; theorem :: XXREAL_1:163 ].r,s.] \/ ].p,q.] c= ].min(r,p),max(s,q).]; theorem :: XXREAL_1:164 ].r,s.] meets ].p,q.] implies ].r,s.] \/ ].p,q.] = ].min(r,p),max(s,q).]; theorem :: XXREAL_1:165 r <= s & s <= t implies [.r,s.] \/ [.s,t.] = [.r,t.]; theorem :: XXREAL_1:166 r <= s & s <= t implies [.r,s.[ \/ [.s,t.] = [.r,t.]; theorem :: XXREAL_1:167 r <= s & s <= t implies [.r,s.] \/ ].s,t.] = [.r,t.]; theorem :: XXREAL_1:168 r <= s & s <= t implies [.r,s.[ \/ [.s,t.[ = [.r,t.[; theorem :: XXREAL_1:169 r <= s & s < t implies [.r,s.] \/ ].s,t.[ = [.r,t.[; theorem :: XXREAL_1:170 r <= s & s <= t implies ].r,s.] \/ ].s,t.] = ].r,t.]; theorem :: XXREAL_1:171 r <= s & s < t implies ].r,s.] \/ ].s,t.[ = ].r,t.[; theorem :: XXREAL_1:172 r < s & s < t implies ].r,s.] \/ [.s,t.[ = ].r,t.[; theorem :: XXREAL_1:173 r < s & s < t implies ].r,s.[ \/ [.s,t.[ = ].r,t.[; theorem :: XXREAL_1:174 p <= s & r <= q & s <= r implies [.p,r.] \/ [.s,q.] = [.p,q.]; theorem :: XXREAL_1:175 p <= s & r <= q & s < r implies [.p,r.[ \/ ].s,q.] = [.p,q.]; theorem :: XXREAL_1:176 p <= s & s <= r & r < q implies [.p,r.] \/ [.s,q.[ = [.p,q.[; theorem :: XXREAL_1:177 p < s & r <= q & s <= r implies ].p,r.] \/ [.s,q.] = ].p,q.]; theorem :: XXREAL_1:178 p < s & r < q & s <= r implies ].p,r.] \/ [.s,q.[ = ].p,q.[; theorem :: XXREAL_1:179 p<=r & p<=s & r<=q & s<=q implies [.p,r.[ \/ [.r,s.] \/ ].s,q.] = [.p,q.]; theorem :: XXREAL_1:180 p -infty implies [.p,-infty.] = {}; theorem :: XXREAL_1:214 :: MEASURE6:37 ].+infty,p.[ = {}; theorem :: XXREAL_1:215 :: MEASURE6:37 [.+infty,p.[ = {}; theorem :: XXREAL_1:216 :: MEASURE6:37 ].+infty,p.] = {}; theorem :: XXREAL_1:217 :: MEASURE6:37 p <> +infty implies [.+infty,p.] = {}; theorem :: XXREAL_1:218 p > q implies p in ].q, +infty.]; theorem :: XXREAL_1:219 q <= p implies p in [.q, +infty.]; theorem :: XXREAL_1:220 p <= q implies p in [.-infty,q.]; theorem :: XXREAL_1:221 p < q implies p in [.-infty, q.[; begin :: Additional theorem :: XXREAL_1:222 p <= q implies [.p,q.] = [.p,q.] \/ [.q,p.]; theorem :: XXREAL_1:223 r <= s & s <= t implies not r in ].s,t.[ \/ ].t,p.[; :: from LIMFUNC1, 2008.06.12, A.T. theorem :: XXREAL_1:224 REAL = ].-infty,+infty.[; theorem :: XXREAL_1:225 ].p,q.[ c= REAL; theorem :: XXREAL_1:226 p in REAL implies [.p,q.[ c= REAL; theorem :: XXREAL_1:227 q in REAL implies ].p,q.] c= REAL; theorem :: XXREAL_1:228 p in REAL & q in REAL implies [.p,q.] c= REAL; registration let p,q; cluster ].p,q.[ -> real-membered; end; registration let p be Real, q; cluster [.p,q.[ -> real-membered; end; registration let q be Real, p; cluster ].p,q.] -> real-membered; end; registration let p,q be Real; cluster [.p,q.] -> real-membered; end; :: from LIMFUNC1,2008.06.13, A.T. theorem :: XXREAL_1:229 ].-infty,s.[ = {g : g