:: TIETZE semantic presentation

theorem Th1: :: TIETZE:1
for b1, b2, b3 being real number st |.(b1 - b2).| <= b3 holds
( b2 - b3 <= b1 & b1 <= b2 + b3 )
proof end;

theorem Th2: :: TIETZE:2
for b1, b2 being real number st b1 < b2 holds
left_closed_halfline b1 misses right_closed_halfline b2
proof end;

theorem Th3: :: TIETZE:3
for b1, b2 being real number st b1 <= b2 holds
left_open_halfline b1 misses right_open_halfline b2
proof end;

theorem Th4: :: TIETZE:4
for b1, b2, b3 being real-yielding Function st b1 c= b2 holds
b3 - b1 c= b3 - b2
proof end;

theorem Th5: :: TIETZE:5
for b1, b2, b3 being real-yielding Function st b1 c= b2 holds
b1 - b3 c= b2 - b3
proof end;

definition
let c1 be real-yielding Function;
let c2 be real number ;
let c3 be set ;
pred c1,c3 is_absolutely_bounded_by c2 means :Def1: :: TIETZE:def 1
for b1 being set st b1 in a3 /\ (dom a1) holds
abs (a1 . b1) <= a2;
end;

:: deftheorem Def1 defines is_absolutely_bounded_by TIETZE:def 1 :
for b1 being real-yielding Function
for b2 being real number
for b3 being set holds
( b1,b3 is_absolutely_bounded_by b2 iff for b4 being set st b4 in b3 /\ (dom b1) holds
abs (b1 . b4) <= b2 );

registration
cluster summable constant convergent Relation of NAT , REAL ;
existence
ex b1 being Real_Sequence st
( b1 is summable & b1 is constant & b1 is convergent )
proof end;
end;

theorem Th6: :: TIETZE:6
for b1 being empty TopSpace
for b2 being TopSpace
for b3 being Function of b1,b2 holds b3 is continuous
proof end;

registration
let c1 be TopSpace;
let c2 be non empty TopSpace;
cluster continuous Relation of the carrier of a1,the carrier of a2;
existence
ex b1 being Function of c1,c2 st b1 is continuous
proof end;
end;

theorem Th7: :: TIETZE:7
for b1, b2 being summable Real_Sequence st ( for b3 being Nat holds b1 . b3 <= b2 . b3 ) holds
Sum b1 <= Sum b2
proof end;

theorem Th8: :: TIETZE:8
for b1 being Real_Sequence st b1 is absolutely_summable holds
abs (Sum b1) <= Sum (abs b1)
proof end;

theorem Th9: :: TIETZE:9
for b1 being Real_Sequence
for b2, b3 being real positive number st b3 < 1 & ( for b4 being natural number holds |.((b1 . b4) - (b1 . (b4 + 1))).| <= b2 * (b3 to_power b4) ) holds
( b1 is convergent & ( for b4 being natural number holds |.((lim b1) - (b1 . b4)).| <= (b2 * (b3 to_power b4)) / (1 - b3) ) )
proof end;

theorem Th10: :: TIETZE:10
for b1 being Real_Sequence
for b2, b3 being real positive number st b3 < 1 & ( for b4 being natural number holds |.((b1 . b4) - (b1 . (b4 + 1))).| <= b2 * (b3 to_power b4) ) holds
( lim b1 >= (b1 . 0) - (b2 / (1 - b3)) & lim b1 <= (b1 . 0) + (b2 / (1 - b3)) )
proof end;

theorem Th11: :: TIETZE:11
for b1, b2 being non empty set
for b3 being Functional_Sequence of b1, REAL st b2 common_on_dom b3 holds
for b4, b5 being real positive number st b5 < 1 & ( for b6 being natural number holds (b3 . b6) - (b3 . (b6 + 1)),b2 is_absolutely_bounded_by b4 * (b5 to_power b6) ) holds
( b3 is_unif_conv_on b2 & ( for b6 being natural number holds (lim b3,b2) - (b3 . b6),b2 is_absolutely_bounded_by (b4 * (b5 to_power b6)) / (1 - b5) ) )
proof end;

theorem Th12: :: TIETZE:12
for b1, b2 being non empty set
for b3 being Functional_Sequence of b1, REAL st b2 common_on_dom b3 holds
for b4, b5 being real positive number st b5 < 1 & ( for b6 being natural number holds (b3 . b6) - (b3 . (b6 + 1)),b2 is_absolutely_bounded_by b4 * (b5 to_power b6) ) holds
for b6 being Element of b2 holds
( (lim b3,b2) . b6 >= ((b3 . 0) . b6) - (b4 / (1 - b5)) & (lim b3,b2) . b6 <= ((b3 . 0) . b6) + (b4 / (1 - b5)) )
proof end;

theorem Th13: :: TIETZE:13
for b1, b2 being non empty set
for b3 being Functional_Sequence of b1, REAL st b2 common_on_dom b3 holds
for b4, b5 being real positive number
for b6 being Function of b2, REAL st b5 < 1 & ( for b7 being natural number holds (b3 . b7) - b6,b2 is_absolutely_bounded_by b4 * (b5 to_power b7) ) holds
( b3 is_point_conv_on b2 & lim b3,b2 = b6 )
proof end;

registration
let c1, c2 be TopStruct ;
let c3 be empty Subset of c1;
let c4 be Function of c1,c2;
cluster a4 | a3 -> empty ;
coherence
c4 | c3 is empty
proof end;
end;

registration
let c1 be TopSpace;
let c2 be closed Subset of c1;
cluster a1 | a2 -> closed ;
coherence
c1 | c2 is closed
proof end;
end;

theorem Th14: :: TIETZE:14
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st ( b3 misses b4 or b5 | (b3 meet b4) = b6 | (b3 meet b4) ) holds
for b7 being Point of b1 holds
( ( b7 in the carrier of b3 implies (b5 union b6) . b7 = b5 . b7 ) & ( b7 in the carrier of b4 implies (b5 union b6) . b7 = b6 . b7 ) )
proof end;

theorem Th15: :: TIETZE:15
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st ( b3 misses b4 or b5 | (b3 meet b4) = b6 | (b3 meet b4) ) holds
rng (b5 union b6) c= (rng b5) \/ (rng b6)
proof end;

theorem Th16: :: TIETZE:16
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st ( b3 misses b4 or b5 | (b3 meet b4) = b6 | (b3 meet b4) ) holds
( ( for b7 being Subset of b3 holds (b5 union b6) .: b7 = b5 .: b7 ) & ( for b7 being Subset of b4 holds (b5 union b6) .: b7 = b6 .: b7 ) )
proof end;

theorem Th17: :: TIETZE:17
for b1 being real number
for b2 being set
for b3, b4 being real-yielding Function st b3 c= b4 & b4,b2 is_absolutely_bounded_by b1 holds
b3,b2 is_absolutely_bounded_by b1
proof end;

theorem Th18: :: TIETZE:18
for b1 being real number
for b2 being set
for b3, b4 being real-yielding Function st ( b2 c= dom b3 or dom b4 c= dom b3 ) & b3 | b2 = b4 | b2 & b3,b2 is_absolutely_bounded_by b1 holds
b4,b2 is_absolutely_bounded_by b1
proof end;

theorem Th19: :: TIETZE:19
for b1 being real number
for b2 being non empty TopSpace
for b3 being closed Subset of b2 st b1 > 0 & b2 is being_T4 holds
for b4 being continuous Function of (b2 | b3),R^1 st b4,b3 is_absolutely_bounded_by b1 holds
ex b5 being continuous Function of b2,R^1 st
( b5, dom b5 is_absolutely_bounded_by b1 / 3 & b4 - b5,b3 is_absolutely_bounded_by (2 * b1) / 3 )
proof end;

theorem Th20: :: TIETZE:20
for b1 being non empty TopSpace st ( for b2, b3 being non empty closed Subset of b1 st b2 misses b3 holds
ex b4 being continuous Function of b1,R^1 st
( b4 .: b2 = {0} & b4 .: b3 = {1} ) ) holds
b1 is_T4
proof end;

theorem Th21: :: TIETZE:21
for b1 being non empty TopSpace
for b2 being Function of b1,R^1
for b3 being Point of b1 holds
( b2 is_continuous_at b3 iff for b4 being real number st b4 > 0 holds
ex b5 being Subset of b1 st
( b5 is open & b3 in b5 & ( for b6 being Point of b1 st b6 in b5 holds
abs ((b2 . b6) - (b2 . b3)) < b4 ) ) )
proof end;

theorem Th22: :: TIETZE:22
for b1 being non empty TopSpace
for b2 being Functional_Sequence of the carrier of b1, REAL st b2 is_unif_conv_on the carrier of b1 & ( for b3 being Nat holds b2 . b3 is continuous Function of b1,R^1 ) holds
lim b2,the carrier of b1 is continuous Function of b1,R^1
proof end;

theorem Th23: :: TIETZE:23
for b1 being non empty TopSpace
for b2 being Function of b1,R^1
for b3 being real positive number holds
( b2,the carrier of b1 is_absolutely_bounded_by b3 iff b2 is Function of b1,(Closed-Interval-TSpace (- b3),b3) )
proof end;

theorem Th24: :: TIETZE:24
for b1 being real number
for b2 being set
for b3, b4 being real-yielding Function st b3 - b4,b2 is_absolutely_bounded_by b1 holds
b4 - b3,b2 is_absolutely_bounded_by b1
proof end;

theorem Th25: :: TIETZE:25
for b1 being non empty TopSpace st b1 is being_T4 holds
for b2 being closed Subset of b1
for b3 being Function of (b1 | b2),(Closed-Interval-TSpace (- 1),1) st b3 is continuous holds
ex b4 being continuous Function of b1,(Closed-Interval-TSpace (- 1),1) st b4 | b2 = b3
proof end;

theorem Th26: :: TIETZE:26
for b1 being non empty TopSpace st ( for b2 being non empty closed Subset of b1
for b3 being continuous Function of (b1 | b2),(Closed-Interval-TSpace (- 1),1) ex b4 being continuous Function of b1,(Closed-Interval-TSpace (- 1),1) st b4 | b2 = b3 ) holds
b1 is being_T4
proof end;