:: On the Simple Closed Curve Property of the Circle and theFashoda Meet Theorem for It
:: by Yatsuka Nakamura
::
:: Received August 20, 2001
:: Copyright (c) 2001 Association of Mizar Users
Lm1:
for x being real number holds (x ^2 ) + 1 > 0
Lm2:
( dom proj1 = the carrier of (TOP-REAL 2) & dom proj2 = the carrier of (TOP-REAL 2) )
by FUNCT_2:def 1;
theorem :: JGRAPH_3:1
canceled;
theorem :: JGRAPH_3:2
canceled;
theorem :: JGRAPH_3:3
canceled;
theorem :: JGRAPH_3:4
canceled;
theorem :: JGRAPH_3:5
canceled;
theorem :: JGRAPH_3:6
canceled;
theorem :: JGRAPH_3:7
canceled;
theorem :: JGRAPH_3:8
canceled;
theorem :: JGRAPH_3:9
canceled;
theorem :: JGRAPH_3:10
theorem :: JGRAPH_3:11
theorem :: JGRAPH_3:12
canceled;
theorem Th13: :: JGRAPH_3:13
definition
func Sq_Circ -> Function of the
carrier of
(TOP-REAL 2),the
carrier of
(TOP-REAL 2) means :
Def1:
:: JGRAPH_3:def 1
for
p being
Point of
(TOP-REAL 2) holds
( (
p = 0.REAL 2 implies
it . p = p ) & ( ( (
p `2 <= p `1 &
- (p `1 ) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1 ) ) ) &
p <> 0.REAL 2 implies
it . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( (
p `2 <= p `1 &
- (p `1 ) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1 ) ) or not
p <> 0.REAL 2 or
it . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) );
existence
ex b1 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds
( ( p = 0.REAL 2 implies b1 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0.REAL 2 implies b1 . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or not p <> 0.REAL 2 or b1 . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) )
uniqueness
for b1, b2 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds
( ( p = 0.REAL 2 implies b1 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0.REAL 2 implies b1 . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or not p <> 0.REAL 2 or b1 . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) ) & ( for p being Point of (TOP-REAL 2) holds
( ( p = 0.REAL 2 implies b2 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0.REAL 2 implies b2 . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or not p <> 0.REAL 2 or b2 . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Sq_Circ JGRAPH_3:def 1 :
theorem Th14: :: JGRAPH_3:14
theorem Th15: :: JGRAPH_3:15
theorem Th16: :: JGRAPH_3:16
theorem Th17: :: JGRAPH_3:17
theorem Th18: :: JGRAPH_3:18
theorem Th19: :: JGRAPH_3:19
theorem Th20: :: JGRAPH_3:20
Lm3:
for K1 being non empty Subset of (TOP-REAL 2)
for q being Point of ((TOP-REAL 2) | K1) holds (proj2 | K1) . q = proj2 . q
Lm4:
for K1 being non empty Subset of (TOP-REAL 2) holds proj2 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1
Lm5:
for K1 being non empty Subset of (TOP-REAL 2)
for q being Point of ((TOP-REAL 2) | K1) holds (proj1 | K1) . q = proj1 . q
Lm6:
for K1 being non empty Subset of (TOP-REAL 2) holds proj1 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1
theorem Th21: :: JGRAPH_3:21
theorem Th22: :: JGRAPH_3:22
theorem Th23: :: JGRAPH_3:23
theorem Th24: :: JGRAPH_3:24
Lm7:
( ( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1 ) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1 ) ) ) & 1.REAL 2 <> 0.REAL 2 )
by JGRAPH_2:13, REVROT_1:19;
Lm8:
for K1 being non empty Subset of (TOP-REAL 2) holds dom (proj2 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)
Lm9:
for K1 being non empty Subset of (TOP-REAL 2) holds dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)
Lm10:
the carrier of (TOP-REAL 2) \ {(0.REAL 2)} <> {}
by JGRAPH_2:19;
theorem Th25: :: JGRAPH_3:25
Lm11:
( ( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2 ) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2 ) ) ) & 1.REAL 2 <> 0.REAL 2 )
by JGRAPH_2:13, REVROT_1:19;
theorem Th26: :: JGRAPH_3:26
theorem Th27: :: JGRAPH_3:27
theorem Th28: :: JGRAPH_3:28
theorem Th29: :: JGRAPH_3:29
theorem Th30: :: JGRAPH_3:30
theorem Th31: :: JGRAPH_3:31
theorem Th32: :: JGRAPH_3:32
theorem Th33: :: JGRAPH_3:33
theorem Th34: :: JGRAPH_3:34
theorem Th35: :: JGRAPH_3:35
theorem :: JGRAPH_3:36
theorem :: JGRAPH_3:37
theorem Th38: :: JGRAPH_3:38
theorem Th39: :: JGRAPH_3:39
theorem Th40: :: JGRAPH_3:40
theorem Th41: :: JGRAPH_3:41
theorem Th42: :: JGRAPH_3:42
theorem Th43: :: JGRAPH_3:43
theorem Th44: :: JGRAPH_3:44
theorem Th45: :: JGRAPH_3:45
theorem Th46: :: JGRAPH_3:46
Lm12:
for K1 being non empty Subset of (TOP-REAL 2) holds proj2 * ((Sq_Circ " ) | K1) is Function of ((TOP-REAL 2) | K1),R^1
Lm13:
for K1 being non empty Subset of (TOP-REAL 2) holds proj1 * ((Sq_Circ " ) | K1) is Function of ((TOP-REAL 2) | K1),R^1
theorem Th47: :: JGRAPH_3:47
theorem Th48: :: JGRAPH_3:48
theorem Th49: :: JGRAPH_3:49
theorem Th50: :: JGRAPH_3:50
theorem Th51: :: JGRAPH_3:51
theorem Th52: :: JGRAPH_3:52
theorem :: JGRAPH_3:53
canceled;
theorem Th54: :: JGRAPH_3:54
theorem :: JGRAPH_3:55