:: by Artur Korni{\l}owicz

::

:: Received June 24, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

registration

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is connected & b_{1} is compact & not b_{1} is vertical & not b_{1} is horizontal )
end;

cluster V23() connected compact non horizontal non vertical for Element of K16( the carrier of (TOP-REAL 2));

existence ex b

( b

proof end;

theorem Th1: :: JORDAN10:1

for i, j, k, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) holds

i < len (Gauge (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,(j + 1)) holds

i < len (Gauge (C,n))

proof end;

theorem Th2: :: JORDAN10:2

for i, j, k, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,(j + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds

i > 1

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,(j + 1)) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds

i > 1

proof end;

theorem Th3: :: JORDAN10:3

for i, j, k, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) holds

j > 1

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (i,j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * ((i + 1),j) holds

j > 1

proof end;

theorem Th4: :: JORDAN10:4

for i, j, k, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((i + 1),j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds

j < width (Gauge (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k + 1 <= len (Cage (C,n)) & [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((i + 1),j) & (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i,j) holds

j < width (Gauge (C,n))

proof end;

theorem Th5: :: JORDAN10:5

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses L~ (Cage (C,n))

proof end;

theorem Th6: :: JORDAN10:6

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))

proof end;

theorem Th7: :: JORDAN10:7

for i, j being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

N-bound (L~ (Cage (C,j))) < N-bound (L~ (Cage (C,i)))

proof end;

registration

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2);

let n be Nat;

coherence

Cl (RightComp (Cage (C,n))) is compact by GOBRD14:32;

end;
let n be Nat;

coherence

Cl (RightComp (Cage (C,n))) is compact by GOBRD14:32;

theorem Th8: :: JORDAN10:8

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min C in RightComp (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-min C in RightComp (Cage (C,n))

proof end;

theorem Th9: :: JORDAN10:9

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C meets RightComp (Cage (C,n))

proof end;

theorem Th10: :: JORDAN10:10

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C misses LeftComp (Cage (C,n))

proof end;

theorem Th11: :: JORDAN10:11

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= RightComp (Cage (C,n))

proof end;

theorem Th12: :: JORDAN10:12

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= BDD (L~ (Cage (C,n)))

proof end;

theorem Th13: :: JORDAN10:13

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C

proof end;

definition

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);

{ (UBD (L~ (Cage (C,n)))) where n is Nat : verum } is set ;

{ (Cl (BDD (L~ (Cage (C,n))))) where n is Nat : verum } is set ;

end;
func UBD-Family C -> set equals :: JORDAN10:def 1

{ (UBD (L~ (Cage (C,n)))) where n is Nat : verum } ;

coherence { (UBD (L~ (Cage (C,n)))) where n is Nat : verum } ;

{ (UBD (L~ (Cage (C,n)))) where n is Nat : verum } is set ;

func BDD-Family C -> set equals :: JORDAN10:def 2

{ (Cl (BDD (L~ (Cage (C,n))))) where n is Nat : verum } ;

coherence { (Cl (BDD (L~ (Cage (C,n))))) where n is Nat : verum } ;

{ (Cl (BDD (L~ (Cage (C,n))))) where n is Nat : verum } is set ;

:: deftheorem defines UBD-Family JORDAN10:def 1 :

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD-Family C = { (UBD (L~ (Cage (C,n)))) where n is Nat : verum } ;

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD-Family C = { (UBD (L~ (Cage (C,n)))) where n is Nat : verum } ;

:: deftheorem defines BDD-Family JORDAN10:def 2 :

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD-Family C = { (Cl (BDD (L~ (Cage (C,n))))) where n is Nat : verum } ;

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD-Family C = { (Cl (BDD (L~ (Cage (C,n))))) where n is Nat : verum } ;

definition

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);

:: original: UBD-Family

redefine func UBD-Family C -> Subset-Family of (TOP-REAL 2);

coherence

UBD-Family C is Subset-Family of (TOP-REAL 2)

redefine func BDD-Family C -> Subset-Family of (TOP-REAL 2);

coherence

BDD-Family C is Subset-Family of (TOP-REAL 2)

end;
:: original: UBD-Family

redefine func UBD-Family C -> Subset-Family of (TOP-REAL 2);

coherence

UBD-Family C is Subset-Family of (TOP-REAL 2)

proof end;

:: original: BDD-Familyredefine func BDD-Family C -> Subset-Family of (TOP-REAL 2);

coherence

BDD-Family C is Subset-Family of (TOP-REAL 2)

proof end;

registration

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);

coherence

not UBD-Family C is empty

not BDD-Family C is empty

end;
coherence

not UBD-Family C is empty

proof end;

coherence not BDD-Family C is empty

proof end;

theorem Th14: :: JORDAN10:14

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds union (UBD-Family C) = UBD C

proof end;

theorem Th15: :: JORDAN10:15

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds C c= meet (BDD-Family C)

proof end;

theorem Th16: :: JORDAN10:16

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses LeftComp (Cage (C,n))

proof end;

theorem Th17: :: JORDAN10:17

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C c= RightComp (Cage (C,n))

proof end;

theorem Th18: :: JORDAN10:18

for n being Nat

for P being Subset of (TOP-REAL 2)

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds

P misses L~ (Cage (C,n))

for P being Subset of (TOP-REAL 2)

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st P is_inside_component_of C holds

P misses L~ (Cage (C,n))

proof end;

theorem Th19: :: JORDAN10:19

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds BDD C misses L~ (Cage (C,n))

proof end;

theorem Th20: :: JORDAN10:20

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds COMPLEMENT (UBD-Family C) = BDD-Family C

proof end;

theorem :: JORDAN10:21

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds meet (BDD-Family C) = C \/ (BDD C)

proof end;