:: Some Properties of Rectangles on the Plane :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received October 18, 2004 :: Copyright (c) 2004-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 NUMBERS, STRUCT_0, TOPMETR, ZFMISC_1, INT_1, ARYTM_3, ARYTM_1, XXREAL_0, XXREAL_1, XBOOLE_0, CARD_1, FUNCT_1, RELAT_1, FINSEQ_1, CARD_3, FUNCOP_1, MONOID_0, PRE_TOPC, PCOMPS_1, EUCLID, SUBSET_1, RCOMP_1, CONNSP_2, TOPS_1, TARSKI, NATTRA_1, TDLAT_3, ORDINAL2, FUNCT_2, T_0TOPSP, TOPS_2, PARTFUN1, REAL_1, FCONT_1, TMAP_1, JGRAPH_6, MCART_1, TOPREALA, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, FUNCOP_1, INT_1, CARD_3, FINSEQ_1, FUNCT_4, MONOID_0, RCOMP_1, FCONT_1, STRUCT_0, PRE_TOPC, PCOMPS_1, TOPS_1, BORSUK_1, TSEP_1, TOPS_2, TDLAT_3, CONNSP_2, T_0TOPSP, TMAP_1, TOPMETR, EUCLID, JGRAPH_6; constructors FUNCT_4, REAL_1, CARD_3, RCOMP_1, FINSEQ_4, FCONT_1, TOPS_1, TOPS_2, TDLAT_3, TMAP_1, T_0TOPSP, MONOID_0, BORSUK_4, JGRAPH_6, FUNCSDOM, PCOMPS_1; registrations RELSET_1, FUNCT_2, FUNCT_4, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, MONOID_0, EUCLID, TOPMETR, TOPGRP_1, VALUED_0, FCONT_1, PCOMPS_1, FUNCT_1, RELAT_1, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin reserve i for Integer, a, b, r, s for Real; registration let r be Real, s be positive Real; cluster ].r,r+s.[ -> non empty; cluster [.r,r+s.[ -> non empty; cluster ].r,r+s.] -> non empty; cluster [.r,r+s.] -> non empty; cluster ].r-s,r.[ -> non empty; cluster [.r-s,r.[ -> non empty; cluster ].r-s,r.] -> non empty; cluster [.r-s,r.] -> non empty; end; registration let r be non positive Real, s be positive Real; cluster ].r,s.[ -> non empty; cluster [.r,s.[ -> non empty; cluster ].r,s.] -> non empty; cluster [.r,s.] -> non empty; end; registration let r be negative Real, s be non negative Real; cluster ].r,s.[ -> non empty; cluster [.r,s.[ -> non empty; cluster ].r,s.] -> non empty; cluster [.r,s.] -> non empty; end; begin :: Functions theorem :: TOPREALA:1 for f being Function, x, X being set st x in dom f & f.x in f.:X & f is one-to-one holds x in X; theorem :: TOPREALA:2 for f being FinSequence, i being Nat st i+1 in dom f holds i in dom f or i = 0; theorem :: TOPREALA:3 for x, y, X, Y being set, f being Function st x <> y & f in product ((x,y) --> (X,Y)) holds f.x in X & f.y in Y; theorem :: TOPREALA:4 for a, b being object holds <*a,b*> = (1,2) --> (a,b); begin :: General topology registration cluster constituted-FinSeqs non empty strict for TopSpace; end; registration let T be constituted-FinSeqs TopSpace; cluster -> constituted-FinSeqs for SubSpace of T; end; theorem :: TOPREALA:5 for T being non empty TopSpace, Z being non empty SubSpace of T, t being Point of T, z being Point of Z, N being open a_neighborhood of t, M being Subset of Z st t = z & M = N /\ [#]Z holds M is open a_neighborhood of z; registration cluster empty -> discrete anti-discrete for TopSpace; end; registration let X be discrete TopSpace, Y be TopSpace; cluster -> continuous for Function of X,Y; end; theorem :: TOPREALA:6 for X being TopSpace, Y being TopStruct, f being Function of X,Y st f is empty holds f is continuous; registration let X be TopSpace, Y be TopStruct; cluster empty -> continuous for Function of X,Y; end; theorem :: TOPREALA:7 for X being TopStruct, Y being non empty TopStruct, Z being non empty SubSpace of Y, f being Function of X,Z holds f is Function of X,Y; theorem :: TOPREALA:8 for S, T being non empty TopSpace, X being Subset of S, Y being Subset of T, f being continuous Function of S,T, g being Function of S|X,T|Y st g = f| X holds g is continuous; theorem :: TOPREALA:9 for S, T being non empty TopSpace, Z being non empty SubSpace of T, f being Function of S,T, g being Function of S,Z st f = g & f is open holds g is open; theorem :: TOPREALA:10 for S, T being non empty TopSpace, S1 being Subset of S, T1 being Subset of T, f being Function of S,T, g being Function of S|S1,T|T1 st g = f|S1 & g is onto & f is open one-to-one holds g is open; theorem :: TOPREALA:11 for X, Y, Z being non empty TopSpace, f being Function of X,Y, g being Function of Y,Z st f is open & g is open holds g*f is open; theorem :: TOPREALA:12 for X, Y being TopSpace, Z being open SubSpace of Y, f being Function of X, Y, g being Function of X, Z st f = g & g is open holds f is open; theorem :: TOPREALA:13 for S, T being non empty TopSpace, f being Function of S,T st f is one-to-one onto holds f is continuous iff f" is open; theorem :: TOPREALA:14 for S, T being non empty TopSpace, f being Function of S,T st f is one-to-one onto holds f is open iff f" is continuous; theorem :: TOPREALA:15 for S being TopSpace, T being non empty TopSpace holds S,T are_homeomorphic iff the TopStruct of S, the TopStruct of T are_homeomorphic; theorem :: TOPREALA:16 for S, T being non empty TopSpace, f being Function of S,T st f is one-to-one onto continuous open holds f is being_homeomorphism; begin :: R^1 theorem :: TOPREALA:17 for f being PartFunc of REAL,REAL st f = REAL --> r holds f|REAL is continuous; theorem :: TOPREALA:18 for f, f1, f2 being PartFunc of REAL,REAL st dom f = dom f1 \/ dom f2 & dom f1 is open & dom f2 is open & f1|dom f1 is continuous & f2|dom f2 is continuous & (for z being set st z in dom f1 holds f.z = f1.z) & (for z being set st z in dom f2 holds f.z = f2.z) holds f|dom f is continuous; theorem :: TOPREALA:19 for x being Point of R^1, N being Subset of REAL, M being Subset of R^1 st M = N holds N is Neighbourhood of x implies M is a_neighborhood of x; theorem :: TOPREALA:20 for x being Point of R^1, M being a_neighborhood of x ex N being Neighbourhood of x st N c= M; theorem :: TOPREALA:21 for f being Function of R^1,R^1, g being PartFunc of REAL,REAL, x being Point of R^1 st f = g & g is_continuous_in x holds f is_continuous_at x ; theorem :: TOPREALA:22 for f being Function of R^1,R^1, g being Function of REAL,REAL st f = g & g is continuous holds f is continuous; theorem :: TOPREALA:23 a <= r & s <= b implies [.r,s.] is closed Subset of Closed-Interval-TSpace(a,b); theorem :: TOPREALA:24 a <= r & s <= b implies ].r,s.[ is open Subset of Closed-Interval-TSpace(a,b) ; theorem :: TOPREALA:25 a <= b & a <= r implies ].r,b.] is open Subset of Closed-Interval-TSpace(a,b) ; theorem :: TOPREALA:26 a <= b & r <= b implies [.a,r.[ is open Subset of Closed-Interval-TSpace(a,b) ; theorem :: TOPREALA:27 a <= b & r <= s implies the carrier of [:Closed-Interval-TSpace( a,b),Closed-Interval-TSpace(r,s):] = [: [.a,b.], [.r,s.] :]; begin :: TOP-REAL 2 theorem :: TOPREALA:28 |[a,b]| = (1,2) --> (a,b); theorem :: TOPREALA:29 |[a,b]|.1 = a & |[a,b]|.2 = b; theorem :: TOPREALA:30 closed_inside_of_rectangle(a,b,r,s) = product ((1,2)-->([.a,b.], [.r,s.])); theorem :: TOPREALA:31 a <= b & r <= s implies |[a,r]| in closed_inside_of_rectangle(a, b,r,s); definition let a, b, c, d be Real; func Trectangle(a,b,c,d) -> SubSpace of TOP-REAL 2 equals :: TOPREALA:def 1 (TOP-REAL 2) | closed_inside_of_rectangle(a,b,c,d); end; theorem :: TOPREALA:32 a <= b & r <= s implies Trectangle(a,b,r,s) is non empty; registration let a, c be non positive Real; let b, d be non negative Real; cluster Trectangle(a,b,c,d) -> non empty; end; definition func R2Homeomorphism -> Function of [:R^1,R^1:], TOP-REAL 2 means :: TOPREALA:def 2 for x, y being Real holds it. [x,y] = <*x,y*>; end; theorem :: TOPREALA:33 for A, B being Subset of REAL holds R2Homeomorphism.:[:A,B:] = product ((1,2) --> (A,B)); theorem :: TOPREALA:34 R2Homeomorphism is being_homeomorphism; theorem :: TOPREALA:35 a <= b & r <= s implies R2Homeomorphism | the carrier of [: Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(r,s):] is Function of [: Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s); theorem :: TOPREALA:36 a <= b & r <= s implies for h being Function of [: Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s) st h = R2Homeomorphism | the carrier of [:Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(r,s):] holds h is being_homeomorphism; theorem :: TOPREALA:37 a <= b & r <= s implies [:Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s) are_homeomorphic; theorem :: TOPREALA:38 a <= b & r <= s implies for A being Subset of Closed-Interval-TSpace(a,b), B being Subset of Closed-Interval-TSpace(r,s) holds product ((1,2)-->(A,B)) is Subset of Trectangle(a,b,r,s); theorem :: TOPREALA:39 a <= b & r <= s implies for A being open Subset of Closed-Interval-TSpace(a,b), B being open Subset of Closed-Interval-TSpace(r,s) holds product ((1,2)-->(A,B)) is open Subset of Trectangle(a,b,r,s); theorem :: TOPREALA:40 a <= b & r <= s implies for A being closed Subset of Closed-Interval-TSpace(a,b), B being closed Subset of Closed-Interval-TSpace(r, s) holds product ((1,2)-->(A,B)) is closed Subset of Trectangle(a,b,r,s);