begin
:: deftheorem Def1 defines is_continuous_in NFCONT_4:def 1 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being real number holds
( f is_continuous_in x0 iff ex g being PartFunc of REAL, the carrier of (REAL-NS n) st
( f = g & g is_continuous_in x0 ) );
theorem Def1Th:
theorem Th1:
theorem Th3:
theorem LM002:
:: deftheorem Def4 defines |. NFCONT_4:def 2 :
for n being Element of NAT
for Z being set
for f being PartFunc of Z,(REAL n)
for b4 being PartFunc of Z,REAL holds
( b4 = |.f.| iff ( dom b4 = dom f & ( for x being set st x in dom b4 holds
b4 /. x = |.(f /. x).| ) ) );
:: deftheorem Def5 defines - NFCONT_4:def 3 :
for n being Element of NAT
for Z being non empty set
for f, b4 being PartFunc of Z,(REAL n) holds
( b4 = - f iff ( dom b4 = dom f & ( for c being set st c in dom b4 holds
b4 /. c = - (f /. c) ) ) );
theorem LM003A:
theorem LM003B:
theorem
theorem LM003E:
theorem LM003F:
theorem LM003D:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th12Y:
:: deftheorem XDef1a defines is_continuous_in NFCONT_4:def 4 :
for n being Element of NAT
for f being PartFunc of (REAL n),REAL
for x0 being Element of REAL n holds
( f is_continuous_in x0 iff ex y0 being Point of (REAL-NS n) ex g being PartFunc of the carrier of (REAL-NS n),REAL st
( x0 = y0 & f = g & g is_continuous_in y0 ) );
theorem Def1aTh:
theorem Th12X:
:: deftheorem Def2 defines continuous NFCONT_4:def 5 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is continuous iff for x0 being real number st x0 in dom f holds
f is_continuous_in x0 );
theorem Def2Th:
theorem Th15:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def6 defines Lipschitzian NFCONT_4:def 6 :
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is Lipschitzian iff ex g being PartFunc of REAL, the carrier of (REAL-NS n) st
( g = f & g is Lipschitzian ) );
theorem Def6Th:
theorem Def6Th1:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem X0:
theorem X1:
theorem
theorem Y0:
theorem Y1:
theorem