:: The Topological Space ${\calE}^2_{\rm T}$.Arcs, Line Segments and Special Polygonal Arcs
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991 Association of Mizar Users
Lm1:
|[0 ,0 ]| = 0.REAL 2
by FINSEQ_2:75;
:: deftheorem TOPREAL1:def 1 :
canceled;
:: deftheorem Def2 defines is_an_arc_of TOPREAL1:def 2 :
theorem :: TOPREAL1:1
canceled;
theorem :: TOPREAL1:2
canceled;
theorem :: TOPREAL1:3
canceled;
theorem Th4: :: TOPREAL1:4
theorem Th5: :: TOPREAL1:5
:: deftheorem Def3 defines LSeg TOPREAL1:def 3 :
for
n being
Nat for
p1,
p2 being
Point of
(TOP-REAL n) holds
LSeg p1,
p2 = { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ;
definition
func R^2-unit_square -> Subset of
(TOP-REAL 2) equals :: TOPREAL1:def 4
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|));
coherence
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|)) is Subset of (TOP-REAL 2)
;
end;
:: deftheorem defines R^2-unit_square TOPREAL1:def 4 :
R^2-unit_square = ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|));
theorem Th6: :: TOPREAL1:6
theorem Th7: :: TOPREAL1:7
theorem Th8: :: TOPREAL1:8
Lm2:
for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg p1,p2 holds
LSeg p1,p c= LSeg p1,p2
theorem :: TOPREAL1:9
theorem :: TOPREAL1:10
theorem Th11: :: TOPREAL1:11
theorem Th12: :: TOPREAL1:12
theorem :: TOPREAL1:13
theorem :: TOPREAL1:14
theorem Th15: :: TOPREAL1:15
theorem Th16: :: TOPREAL1:16
theorem Th17: :: TOPREAL1:17
theorem :: TOPREAL1:18
theorem Th19: :: TOPREAL1:19
(
LSeg |[0 ,0 ]|,
|[0 ,1]| = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = 0 & p1 `2 <= 1 & p1 `2 >= 0 ) } &
LSeg |[0 ,1]|,
|[1,1]| = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } &
LSeg |[0 ,0 ]|,
|[1,0 ]| = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } &
LSeg |[1,0 ]|,
|[1,1]| = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )
theorem :: TOPREAL1:20
theorem :: TOPREAL1:21
theorem :: TOPREAL1:22
theorem Th23: :: TOPREAL1:23
theorem Th24: :: TOPREAL1:24
theorem :: TOPREAL1:25
theorem Th26: :: TOPREAL1:26
:: deftheorem Def5 defines LSeg TOPREAL1:def 5 :
theorem Th27: :: TOPREAL1:27
:: deftheorem defines L~ TOPREAL1:def 6 :
theorem Th28: :: TOPREAL1:28
theorem Th29: :: TOPREAL1:29
:: deftheorem defines special TOPREAL1:def 7 :
:: deftheorem Def8 defines unfolded TOPREAL1:def 8 :
:: deftheorem Def9 defines s.n.c. TOPREAL1:def 9 :
:: deftheorem Def10 defines being_S-Seq TOPREAL1:def 10 :
theorem Th30: :: TOPREAL1:30
theorem Th31: :: TOPREAL1:31
:: deftheorem Def11 defines being_S-P_arc TOPREAL1:def 11 :
theorem Th32: :: TOPREAL1:32
theorem :: TOPREAL1:33
canceled;
theorem :: TOPREAL1:34
theorem Th35: :: TOPREAL1:35
theorem :: TOPREAL1:36
:: deftheorem Def12 defines north_halfline TOPREAL1:def 12 :
:: deftheorem Def13 defines east_halfline TOPREAL1:def 13 :
:: deftheorem Def14 defines south_halfline TOPREAL1:def 14 :
:: deftheorem Def15 defines west_halfline TOPREAL1:def 15 :
theorem :: TOPREAL1:37
theorem Th38: :: TOPREAL1:38
theorem :: TOPREAL1:39
theorem Th40: :: TOPREAL1:40
theorem :: TOPREAL1:41
theorem Th42: :: TOPREAL1:42
theorem :: TOPREAL1:43
theorem Th44: :: TOPREAL1:44
theorem :: TOPREAL1:45