Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Robert Milewski
- Received September 27, 2003
- MML identifier: JORDAN19
- [
Mizar article,
MML identifier index
]
environ
vocabulary JORDAN19, JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1,
GOBOARD5, JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, GROUP_2, NAT_1,
SPPOL_2, REALSET1, JORDAN1E, SQUARE_1, FINSEQ_4, TOPREAL2, CONNSP_1,
COMPTS_1, TOPREAL1, SPPOL_1, FINSEQ_1, TREES_1, EUCLID, RELAT_1, MCART_1,
MATRIX_1, GOBOARD9, PRE_TOPC, RELAT_2, SEQM_3, SUBSET_1, FUNCT_1,
ARYTM_1, FINSEQ_6, GOBOARD2, GROUP_1, GRAPH_2, METRIC_1, ARYTM, ORDINAL2,
ARYTM_3, INT_1, FUNCT_5, ABSVALUE, CONNSP_2, COMPLEX1, POWER, TOPS_1,
KURATO_2, PROB_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0,
REAL_1, INT_1, NAT_1, SQUARE_1, FUNCT_1, FUNCT_2, LIMFUNC1, ABSVALUE,
FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_1, FINSEQ_6, POWER, TOPRNS_1,
METRIC_1, CONNSP_2, GRAPH_2, STRUCT_0, REALSET1, PRE_TOPC, TOPS_1,
TOPREAL2, CARD_4, BINARITH, PROB_1, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1,
SPRECT_2, SPPOL_2, KURATO_2, GOBOARD1, GOBRD14, TOPREAL1, GOBOARD2,
GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN3, JORDAN6, JORDAN8, JORDAN9,
JORDAN2C, JORDAN1A, JORDAN1E;
constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1,
BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, FINSEQ_4, JORDAN1,
JORDAN3, TOPREAL2, JORDAN5C, GRAPH_2, SPRECT_1, GOBOARD2, TOPS_1,
FINSOP_1, JORDAN1E, WSIERP_1, JORDAN1H, ABSVALUE, CONNSP_2, LIMFUNC1,
TOPRNS_1, SERIES_1, GOBRD14, DOMAIN_1, KURATO_2, INT_1;
clusters SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1, REAL_1,
SUBSET_1, SPRECT_3, GOBOARD2, FINSEQ_5, SPPOL_2, JORDAN1A, JORDAN1B,
JORDAN1G, GOBRD11, FUNCT_7, XBOOLE_0, EUCLID, PSCOMP_1, JORDAN1J,
METRIC_1, XREAL_0, ORDINAL2;
requirements NUMERALS, ARITHM, BOOLE, SUBSET, REAL;
begin
reserve n for Nat;
definition
let C be Simple_closed_curve;
func Upper_Appr C -> SetSequence of the carrier of TOP-REAL 2 means
:: JORDAN19:def 1
for i be Nat holds it.i = Upper_Arc L~Cage (C,i);
func Lower_Appr C -> SetSequence of the carrier of TOP-REAL 2 means
:: JORDAN19:def 2
for i being Nat holds it.i = Lower_Arc L~Cage (C,i);
end;
definition
let C be Simple_closed_curve;
func North_Arc C -> Subset of TOP-REAL 2 equals
:: JORDAN19:def 3
Lim_inf Upper_Appr C;
func South_Arc C -> Subset of TOP-REAL 2 equals
:: JORDAN19:def 4
Lim_inf Lower_Appr C;
end;
theorem :: JORDAN19:1
for n,m be Nat holds n <= m & n <> 0 implies (n+1)/n >= (m+1)/m;
theorem :: JORDAN19:2
for E be compact non vertical non horizontal Subset of TOP-REAL 2
for m,j be Nat st 1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) holds
LSeg(Gauge(E,n)*(Center Gauge(E,n),width Gauge(E,n)),
Gauge(E,n)*(Center Gauge(E,n),j)) c=
LSeg(Gauge(E,m)*(Center Gauge(E,m),width Gauge(E,m)),
Gauge(E,n)*(Center Gauge(E,n),j));
theorem :: JORDAN19:3
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for i,j be Nat st 1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,width Gauge(C,n)),Gauge(C,n)*(i,j)) meets
L~Upper_Seq(C,n);
theorem :: JORDAN19:4
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for n be Nat st n > 0
for i,j be Nat st 1 <= i & i <= len Gauge(C,n) &
1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,width Gauge(C,n)),Gauge(C,n)*(i,j)) meets
Upper_Arc L~Cage(C,n);
theorem :: JORDAN19:5
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for j be Nat holds
Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) &
1 <= j & j <= width Gauge(C,n+1) implies
LSeg(Gauge(C,1)*(Center Gauge(C,1),width Gauge(C,1)),
Gauge(C,n+1)*(Center Gauge(C,n+1),j)) meets Upper_Arc L~Cage(C,n+1);
theorem :: JORDAN19:6
for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
for f be FinSequence of TOP-REAL 2
for k be Nat st 1 <= k & k+1 <= len f & f is_sequence_on Gauge(C,n) holds
dist(f/.k,f/.(k+1)) = (N-bound C - S-bound C)/2|^n or
dist(f/.k,f/.(k+1)) = (E-bound C - W-bound C)/2|^n;
theorem :: JORDAN19:7
for M be symmetric triangle MetrStruct
for r be real number
for p,q,x be Element of M st
p in Ball(x,r) & q in Ball(x,r) holds
dist(p,q) < 2*r;
theorem :: JORDAN19:8
for A be Subset of TOP-REAL n
for p be Point of TOP-REAL n
for p' be Point of Euclid n st p = p'
for s be real number st s > 0 holds
p in Cl A iff
for r be real number st 0 < r & r < s holds Ball (p',r) meets A;
theorem :: JORDAN19:9
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
N-bound C < N-bound L~Cage(C,n);
theorem :: JORDAN19:10
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
E-bound C < E-bound L~Cage(C,n);
theorem :: JORDAN19:11
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
S-bound L~Cage(C,n) < S-bound C;
theorem :: JORDAN19:12
for C be compact connected non vertical non horizontal
Subset of TOP-REAL 2 holds
W-bound L~Cage(C,n) < W-bound C;
theorem :: JORDAN19:13
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= k & k <= j & j <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) meets Upper_Arc C;
theorem :: JORDAN19:14
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= k & k <= j & j <= width Gauge(C,n) &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,k),Gauge(C,n)*(i,j)) meets Lower_Arc C;
theorem :: JORDAN19:15
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;
theorem :: JORDAN19:16
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,k)} &
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
{Gauge(C,n)*(i,j)} holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;
theorem :: JORDAN19:17
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;
theorem :: JORDAN19:18
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) &
Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;
theorem :: JORDAN19:19
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;
theorem :: JORDAN19:20
for C be Simple_closed_curve
for i,j,k be Nat st
1 < i & i < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
Gauge(C,n)*(i,k) in Lower_Arc L~Cage(C,n) &
Gauge(C,n)*(i,j) in Upper_Arc L~Cage(C,n) holds
LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;
theorem :: JORDAN19:21
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i1,j)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i2,k)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C;
theorem :: JORDAN19:22
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i1,j)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i2,k)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C;
theorem :: JORDAN19:23
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i1,j)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i2,k)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C;
theorem :: JORDAN19:24
for C be Simple_closed_curve
for i1,i2,j,k be Nat st
1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) &
1 <= j & j <= k & k <= width Gauge(C,n) &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Upper_Seq(C,n) =
{Gauge(C,n)*(i1,j)} &
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~Lower_Seq(C,n) =
{Gauge(C,n)*(i2,k)} holds
(LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/
LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C;
theorem :: JORDAN19:25
for C be Simple_closed_curve
for i1,i2,j,k be Nat holds
1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) &
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(i1,k) in Lower_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(i2,j) in Upper_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(i2,j),Gauge(C,n+1)*(i2,k)) \/
LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Lower_Arc C;
theorem :: JORDAN19:26
for C be Simple_closed_curve
for i1,i2,j,k be Nat holds
1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) &
1 <= j & j <= k & k <= width Gauge(C,n+1) &
Gauge(C,n+1)*(i1,k) in Lower_Arc L~Cage(C,n+1) &
Gauge(C,n+1)*(i2,j) in Upper_Arc L~Cage(C,n+1) implies
LSeg(Gauge(C,n+1)*(i2,j),Gauge(C,n+1)*(i2,k)) \/
LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Upper_Arc C;
theorem :: JORDAN19:27
for C be Simple_closed_curve
for p be Point of TOP-REAL 2 st W-bound C < p`1 & p`1 < E-bound C holds
not(p in North_Arc C & p in South_Arc C);
theorem :: JORDAN19:28 :: "Nie oba"
for C be Simple_closed_curve
for p be Point of TOP-REAL 2 st p`1 = (W-bound C + E-bound C)/2 holds
not (p in North_Arc C & p in South_Arc C);
Back to top