:: FRECHET2 semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
Lm1:
for T being non empty TopSpace holds
( T is_T1 iff for p being Point of T holds Cl {p} = {p} )
Lm2:
for T being non empty TopSpace st not T is_T1 holds
ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
Lm3:
for T being non empty TopSpace st not T is_T1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 )
Lm4:
for T being non empty TopSpace st T is_T2 holds
T is_T1
Lm5:
for T being non empty 1-sorted
for S being sequence of T
for f being Function of NAT , NAT holds S * f is sequence of T
;
theorem Th1: :: FRECHET2:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm6:
id NAT is Real_Sequence
Lm7:
for RS being Real_Sequence st RS = id NAT holds
RS is natural-yielding
Lm8:
for RS being Real_Sequence st RS = id NAT holds
RS is increasing
theorem :: FRECHET2:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm9:
for T being non empty 1-sorted
for S being sequence of T ex NS being increasing Seq_of_Nat st S = S * NS
theorem Th3: :: FRECHET2:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th4: :: FRECHET2:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm10:
for T being non empty 1-sorted
for S being sequence of T
for NS being increasing Seq_of_Nat holds S * NS is subsequence of S
theorem Th5: :: FRECHET2:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th6: :: FRECHET2:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: FRECHET2:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm11:
for T being non empty TopSpace st T is first-countable holds
for x being Point of T ex B being Basis of x ex S being Function st
( dom S = NAT & rng S = B & ( for n, m being Nat st m >= n holds
S . m c= S . n ) )
theorem :: FRECHET2:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th9: :: FRECHET2:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th11: :: FRECHET2:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th12: :: FRECHET2:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th14: :: FRECHET2:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem FRECHET2:def 1 :
canceled;
:: deftheorem Def2 defines Cl_Seq FRECHET2:def 2 :
theorem Th16: :: FRECHET2:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th17: :: FRECHET2:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th18: :: FRECHET2:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th19: :: FRECHET2:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th20: :: FRECHET2:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th21: :: FRECHET2:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th22: :: FRECHET2:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th23: :: FRECHET2:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th24: :: FRECHET2:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th25: :: FRECHET2:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def3 defines lim FRECHET2:def 3 :
theorem Th27: :: FRECHET2:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th28: :: FRECHET2:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th31: :: FRECHET2:31 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:32 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:33 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def4 defines is_a_cluster_point_of FRECHET2:def 4 :
theorem Th34: :: FRECHET2:34 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:35 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th36: :: FRECHET2:36 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th37: :: FRECHET2:37 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th38: :: FRECHET2:38 :: Showing IDV graph ... (Click the Palm Tree again to close it)
Lm12:
for f being Function st not dom f is finite & f is one-to-one holds
not rng f is finite
theorem Th39: :: FRECHET2:39 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th40: :: FRECHET2:40 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th41: :: FRECHET2:41 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th42: :: FRECHET2:42 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th43: :: FRECHET2:43 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th44: :: FRECHET2:44 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:45 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:46 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:47 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:48 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:49 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: FRECHET2:50 :: Showing IDV graph ... (Click the Palm Tree again to close it)