:: NFCONT_2 semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem Def1 defines is_uniformly_continuous_on NFCONT_2:def 1 :
:: deftheorem Def2 defines is_uniformly_continuous_on NFCONT_2:def 2 :
theorem Th1: :: NFCONT_2:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th4: :: NFCONT_2:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th7: :: NFCONT_2:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th8: :: NFCONT_2:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th9: :: NFCONT_2:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def3 defines contraction NFCONT_2:def 3 :
Lm1:
( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )
Lm2:
for K, L, e being real number st 0 < K & K < 1 & 0 < e holds
ex n being Nat st abs (L * (K to_power n)) < e
theorem Th14: :: NFCONT_2:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: NFCONT_2:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)