:: 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);