:: UNIFORM1 semantic presentation

theorem Th1: :: UNIFORM1:1

canceled;

theorem Th2: :: UNIFORM1:2

for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
( b₂ > 0 & 1 / b₂ < b₁ )

proof end;

definition

let c₁, c₂ be non empty MetrStruct ;
let c₃ be Function of c₁,c₂;
attr a₃ is uniformly_continuous means :Def1: :: UNIFORM1:def 1
for b₁ being Real st 0 < b₁ holds
ex b₂ being Real st
( 0 < b₂ & ( for b₃, b₄ being Element of a₁ st dist b₃,b₄ < b₂ holds
dist (a₃ /. b₃),(a₃ /. b₄) < b₁ ) );

end;

:: deftheorem Def1 defines uniformly_continuous UNIFORM1:def 1 :

theorem Th3: :: UNIFORM1:3

for b₁ being non empty TopSpace
for b₂ being non empty MetrSpace
for b₃ being Function of b₁,(TopSpaceMetr b₂) st b₃ is continuous holds
for b₄ being Real
for b₅ being Element of the carrier of b₂
for b₆ being Subset of (TopSpaceMetr b₂) st b₆ = Ball b₅,b₄ holds
b₃ " b₆ is open

proof end;

theorem Th4: :: UNIFORM1:4

for b₁, b₂ being non empty MetrSpace
for b₃ being Function of (TopSpaceMetr b₁),(TopSpaceMetr b₂) st ( for b₄ being real number
for b₅ being Element of the carrier of b₁
for b₆ being Element of b₂ st b₄ > 0 & b₆ = b₃ . b₅ holds
ex b₇ being real number st
( b₇ > 0 & ( for b₈ being Element of b₁
for b₉ being Element of b₂ st b₉ = b₃ . b₈ & dist b₅,b₈ < b₇ holds
dist b₆,b₉ < b₄ ) ) ) holds
b₃ is continuous

proof end;

theorem Th5: :: UNIFORM1:5

for b₁, b₂ being non empty MetrSpace
for b₃ being Function of (TopSpaceMetr b₁),(TopSpaceMetr b₂) st b₃ is continuous holds
for b₄ being Real
for b₅ being Element of the carrier of b₁
for b₆ being Element of b₂ st b₄ > 0 & b₆ = b₃ . b₅ holds
ex b₇ being Real st
( b₇ > 0 & ( for b₈ being Element of b₁
for b₉ being Element of b₂ st b₉ = b₃ . b₈ & dist b₅,b₈ < b₇ holds
dist b₆,b₉ < b₄ ) )

proof end;

theorem Th6: :: UNIFORM1:6

for b₁, b₂ being non empty MetrSpace
for b₃ being Function of b₁,b₂
for b₄ being Function of (TopSpaceMetr b₁),(TopSpaceMetr b₂) st b₃ = b₄ & b₃ is uniformly_continuous holds
b₄ is continuous

proof end;

theorem Th7: :: UNIFORM1:7

for b₁ being non empty MetrSpace
for b₂ being Subset-Family of (TopSpaceMetr b₁) st b₂ is_a_cover_of TopSpaceMetr b₁ & b₂ is open & TopSpaceMetr b₁ is compact holds
ex b₃ being Real st
( b₃ > 0 & ( for b₄, b₅ being Element of b₁ st dist b₄,b₅ < b₃ holds
ex b₆ being Subset of (TopSpaceMetr b₁) st
( b₄ in b₆ & b₅ in b₆ & b₆ in b₂ ) ) )

proof end;

theorem Th8: :: UNIFORM1:8

for b₁, b₂ being non empty MetrSpace
for b₃ being Function of b₁,b₂
for b₄ being Function of (TopSpaceMetr b₁),(TopSpaceMetr b₂) st b₄ = b₃ & TopSpaceMetr b₁ is compact & b₄ is continuous holds
b₃ is uniformly_continuous

proof end;

Lemma8: Closed-Interval-TSpace 0,1 = TopSpaceMetr (Closed-Interval-MSpace 0,1)
by TOPMETR:def 8;

Lemma9: I[01] = TopSpaceMetr (Closed-Interval-MSpace 0,1)
by TOPMETR:27, TOPMETR:def 8;

Lemma10: the carrier of I[01] = the carrier of (Closed-Interval-MSpace 0,1)
by Lemma8, TOPMETR:16, TOPMETR:27;

theorem Th9: :: UNIFORM1:9

for b₁ being Nat
for b₂ being Function of I[01] ,(TOP-REAL b₁)
for b₃ being Function of (Closed-Interval-MSpace 0,1),(Euclid b₁) st b₂ is continuous & b₃ = b₂ holds
b₃ is uniformly_continuous by Lemma8, Th8, TOPMETR:27;

theorem Th10: :: UNIFORM1:10

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃ being non empty Subset of (Euclid b₁)
for b₄ being Function of I[01] ,((TOP-REAL b₁) | b₂)
for b₅ being Function of (Closed-Interval-MSpace 0,1),((Euclid b₁) | b₃) st b₂ = b₃ & b₄ is continuous & b₅ = b₄ holds
b₅ is uniformly_continuous

proof end;

theorem Th11: :: UNIFORM1:11

for b₁ being Nat
for b₂ being Function of I[01] ,(TOP-REAL b₁) ex b₃ being Function of (Closed-Interval-MSpace 0,1),(Euclid b₁) st b₃ = b₂

proof end;

Lemma13: for b₁ being set
for b₂ being FinSequence holds
( len (b₂ ^ <*b₁*>) = (len b₂) + 1 & len (<*b₁*> ^ b₂) = (len b₂) + 1 & (b₂ ^ <*b₁*>) . ((len b₂) + 1) = b₁ & (<*b₁*> ^ b₂) . 1 = b₁ )

proof end;

Lemma14: for b₁ being set
for b₂ being FinSequence st 1 <= len b₂ holds
( (b₂ ^ <*b₁*>) . 1 = b₂ . 1 & (<*b₁*> ^ b₂) . ((len b₂) + 1) = b₂ . (len b₂) )

proof end;

theorem Th12: :: UNIFORM1:12

canceled;

theorem Th13: :: UNIFORM1:13

for b₁, b₂ being Real holds abs (b₁ - b₂) = abs (b₂ - b₁)

proof end;

Lemma16: for b₁, b₂, b₃ being Real holds
( b₁ in [.b₂,b₃.] iff ( b₂ <= b₁ & b₁ <= b₃ ) )

proof end;

theorem Th14: :: UNIFORM1:14

for b₁, b₂, b₃, b₄ being Real st b₁ in [.b₃,b₄.] & b₂ in [.b₃,b₄.] holds
abs (b₁ - b₂) <= b₄ - b₃

proof end;

definition

let c₁ be FinSequence of REAL ;
attr a₁ is decreasing means :Def2: :: UNIFORM1:def 2
for b₁, b₂ being Nat st b₁ in dom a₁ & b₂ in dom a₁ & b₁ < b₂ holds
a₁ . b₁ > a₁ . b₂;

end;

:: deftheorem Def2 defines decreasing UNIFORM1:def 2 :

Lemma19: for b₁ being FinSequence of REAL st ( for b₂ being Nat st 1 <= b₂ & b₂ < len b₁ holds
b₁ /. b₂ < b₁ /. (b₂ + 1) ) holds
b₁ is increasing

proof end;

Lemma20: for b₁ being FinSequence of REAL st ( for b₂ being Nat st 1 <= b₂ & b₂ < len b₁ holds
b₁ /. b₂ > b₁ /. (b₂ + 1) ) holds
b₁ is decreasing

proof end;

theorem Th15: :: UNIFORM1:15

for b₁ being Nat
for b₂ being Real
for b₃ being Function of I[01] ,(TOP-REAL b₁)
for b₄, b₅ being Element of (TOP-REAL b₁) st b₂ > 0 & b₃ is continuous & b₃ is one-to-one & b₃ . 0 = b₄ & b₃ . 1 = b₅ holds
ex b₆ being FinSequence of REAL st
( b₆ . 1 = 0 & b₆ . (len b₆) = 1 & 5 <= len b₆ & rng b₆ c= the carrier of I[01] & b₆ is increasing & ( for b₇ being Nat
for b₈ being Subset of I[01]
for b₉ being Subset of (Euclid b₁) st 1 <= b₇ & b₇ < len b₆ & b₈ = [.(b₆ /. b₇),(b₆ /. (b₇ + 1)).] & b₉ = b₃ .: b₈ holds
diameter b₉ < b₂ ) )

proof end;

theorem Th16: :: UNIFORM1:16

for b₁ being Nat
for b₂ being Real
for b₃ being Function of I[01] ,(TOP-REAL b₁)
for b₄, b₅ being Element of (TOP-REAL b₁) st b₂ > 0 & b₃ is continuous & b₃ is one-to-one & b₃ . 0 = b₄ & b₃ . 1 = b₅ holds
ex b₆ being FinSequence of REAL st
( b₆ . 1 = 1 & b₆ . (len b₆) = 0 & 5 <= len b₆ & rng b₆ c= the carrier of I[01] & b₆ is decreasing & ( for b₇ being Nat
for b₈ being Subset of I[01]
for b₉ being Subset of (Euclid b₁) st 1 <= b₇ & b₇ < len b₆ & b₈ = [.(b₆ /. (b₇ + 1)),(b₆ /. b₇).] & b₉ = b₃ .: b₈ holds
diameter b₉ < b₂ ) )

proof end;