:: Upper and Lower Sequence of a Cage
:: by Robert Milewski
::
:: Received August 8, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem :: JORDAN1E:1
canceled;
theorem :: JORDAN1E:2
canceled;
theorem :: JORDAN1E:3
canceled;
theorem :: JORDAN1E:4
canceled;
theorem Th5: :: JORDAN1E:5
theorem Th6: :: JORDAN1E:6
theorem :: JORDAN1E:7
theorem :: JORDAN1E:8
theorem Th9: :: JORDAN1E:9
theorem Th10: :: JORDAN1E:10
theorem :: JORDAN1E:11
:: deftheorem defines Upper_Seq JORDAN1E:def 1 :
theorem Th12: :: JORDAN1E:12
:: deftheorem defines Lower_Seq JORDAN1E:def 2 :
theorem Th13: :: JORDAN1E:13
registration
let C be
compact non
horizontal non
vertical Subset of
(TOP-REAL 2);
let n be
Element of
NAT ;
cluster Upper_Seq C,
n -> one-to-one special unfolded s.n.c. ;
coherence
( Upper_Seq C,n is one-to-one & Upper_Seq C,n is special & Upper_Seq C,n is unfolded & Upper_Seq C,n is s.n.c. )
cluster Lower_Seq C,
n -> one-to-one special unfolded s.n.c. ;
coherence
( Lower_Seq C,n is one-to-one & Lower_Seq C,n is special & Lower_Seq C,n is unfolded & Lower_Seq C,n is s.n.c. )
end;
theorem Th14: :: JORDAN1E:14
theorem Th15: :: JORDAN1E:15
theorem :: JORDAN1E:16
theorem :: JORDAN1E:17
theorem Th18: :: JORDAN1E:18
theorem Th19: :: JORDAN1E:19
theorem :: JORDAN1E:20
theorem :: JORDAN1E:21
theorem :: JORDAN1E:22
theorem :: JORDAN1E:23
theorem :: JORDAN1E:24
theorem :: JORDAN1E:25
theorem :: JORDAN1E:26