The abstract of the Mizar article:

Properties of Real Functions

by

Jaroslaw Kotowicz

Received June 18, 1990

MML identifier: RFUNCT_2

[ Mizar article, MML identifier index ]

environ

 vocabulary SEQ_1, ORDINAL2, SEQM_3, PARTFUN1, FUNCT_1, RELAT_1, BOOLE,
      ARYTM_1, ABSVALUE, SEQ_2, ARYTM, FINSEQ_1, LATTICES, SEQ_4, PARTFUN2,
      RCOMP_1, RFUNCT_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, RELAT_1, FUNCT_1, SEQ_1, SEQ_2, SEQ_4, RELSET_1, ABSVALUE,
      PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, SEQM_3;
 constructors REAL_1, NAT_1, SEQ_2, SEQM_3, SEQ_4, ABSVALUE, PARTFUN1,
      PARTFUN2, RCOMP_1, RFUNCT_1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, RELSET_1, PARTFUN2, XREAL_0, SEQ_1, SEQM_3, MEMBERED,
      ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve x,y,X,X1,Y for set;
 reserve g,r,r1,r2,p,p1,p2 for Element of REAL;
 reserve R for Subset of REAL;
 reserve seq,seq1,seq2,seq3 for Real_Sequence;
 reserve Ns for increasing Seq_of_Nat;
 reserve n,m for Element of NAT;
 reserve h,h1,h2 for PartFunc of REAL,REAL;

canceled;

theorem :: RFUNCT_2:2
  for F,G be Function, X holds (G|(F.:X))*(F|X) = (G*F)|X;

theorem :: RFUNCT_2:3
  for F,G be Function, X,X1 holds (G|X1)*(F|X) = (G*F)|(X /\ (F"X1));

theorem :: RFUNCT_2:4
for F,G be Function,X holds X c= dom (G*F) iff X c= dom F & F.:X c= dom G;

theorem :: RFUNCT_2:5
  for F be Function, X holds (F|X).:X=F.:X;

::
:: REAL SEQUENCES
::

definition let seq;
  redefine func rng seq -> Subset of REAL;
end;

theorem :: RFUNCT_2:6
seq1=seq2-seq3 iff for n holds seq1.n=seq2.n-seq3.n;

theorem :: RFUNCT_2:7
rng (seq^\n) c= rng seq;

theorem :: RFUNCT_2:8
rng seq c= dom h implies seq.n in dom h;

theorem :: RFUNCT_2:9
x in rng seq iff ex n st x = seq.n;

theorem :: RFUNCT_2:10
  seq.n in rng seq;

theorem :: RFUNCT_2:11
seq1 is_subsequence_of seq implies rng seq1 c= rng seq;

theorem :: RFUNCT_2:12
  seq1 is_subsequence_of seq & seq is_not_0 implies seq1 is_not_0;

theorem :: RFUNCT_2:13
(seq1 + seq2)*Ns = (seq1*Ns) + (seq2*Ns) &
(seq1 - seq2)*Ns = (seq1*Ns) - (seq2*Ns) &
(seq1 (#) seq2)*Ns = (seq1*Ns) (#) (seq2*Ns);

theorem :: RFUNCT_2:14
(p(#)seq)*Ns = p(#)(seq*Ns);

theorem :: RFUNCT_2:15
  (-seq)*Ns = -(seq*Ns) & (abs(seq))*Ns = abs((seq*Ns));

theorem :: RFUNCT_2:16
  (seq*Ns)" = (seq")*Ns;

theorem :: RFUNCT_2:17
  (seq1/"seq)*Ns = (seq1*Ns)/"(seq*Ns);

theorem :: RFUNCT_2:18
  seq is convergent & (for n holds seq.n<=0) implies lim seq <= 0;

theorem :: RFUNCT_2:19
  (for n holds seq.n in Y) implies rng seq c= Y;

definition let h,seq;
assume  rng seq c= dom h;
func h*seq -> Real_Sequence equals
:: RFUNCT_2:def 1
(h qua Function)*seq;
end;

canceled;

theorem :: RFUNCT_2:21
rng seq c= dom h implies (h*seq).n = h.(seq.n);

theorem :: RFUNCT_2:22
rng seq c= dom h implies (h*seq)^\n=h*(seq^\n);

theorem :: RFUNCT_2:23
rng seq c= dom h1 /\ dom h2 implies (h1+h2)*seq=h1*seq+h2*seq &
                                   (h1-h2)*seq=h1*seq-h2*seq &
                                   (h1(#)h2)*seq=(h1*seq)(#)(h2*seq);

theorem :: RFUNCT_2:24
for r being real number holds rng seq c= dom h implies (r(#)h)*seq = r(#)
(h*seq);

theorem :: RFUNCT_2:25
  rng seq c= dom h implies abs(h*seq) = (abs(h))*seq & -(h*seq) = (-h)*seq;

theorem :: RFUNCT_2:26
  rng seq c= dom (h^) implies h*seq is_not_0;

theorem :: RFUNCT_2:27
  rng seq c= dom (h^) implies (h^)*seq =(h*seq)";

theorem :: RFUNCT_2:28
rng seq c= dom h implies (h*seq)*Ns = h * (seq*Ns);

theorem :: RFUNCT_2:29
  rng seq1 c= dom h & seq2 is_subsequence_of seq1 implies
  h*seq2 is_subsequence_of h*seq1;

theorem :: RFUNCT_2:30
  h is total implies (h*seq).n = h.(seq.n);

theorem :: RFUNCT_2:31
  h is total implies h*(seq^\n) = (h*seq)^\n;

theorem :: RFUNCT_2:32
  h1 is total & h2 is total implies (h1+h2)*seq = h1*seq + h2*seq &
(h1-h2)*seq = h1*seq - h2*seq & (h1(#)h2)*seq = (h1*seq) (#) (h2*seq);

theorem :: RFUNCT_2:33
  h is total implies (r(#)h)*seq = r(#)(h*seq);

theorem :: RFUNCT_2:34
  rng seq c= dom (h|X) implies (h|X)*seq = h*seq;

theorem :: RFUNCT_2:35
  rng seq c= dom (h|X) & (rng seq c= dom (h|Y) or X c= Y) implies
 (h|X)*seq = (h|Y)*seq;

theorem :: RFUNCT_2:36
  rng seq c= dom (h|X) implies abs((h|X)*seq) = ((abs(h))|X)*seq;

theorem :: RFUNCT_2:37
  rng seq c= dom (h|X) & h"{0}={} implies ((h^)|X)*seq = ((h|X)*seq)";

theorem :: RFUNCT_2:38
rng seq c= dom h implies h.:(rng seq) = rng (h*seq);

theorem :: RFUNCT_2:39
  rng seq c= dom (h2*h1) implies h2*(h1*seq) = h2*h1*seq;

::
:: MONOTONE FUNCTIONS
::

definition let Z be set;
 let f be one-to-one Function;
 cluster f|Z -> one-to-one;
end;

theorem :: RFUNCT_2:40
   for h being one-to-one Function holds (h|X)" = (h")|(h.:X);

theorem :: RFUNCT_2:41
rng h is bounded & upper_bound (rng h) = lower_bound (rng h) implies
h is_constant_on dom h;

theorem :: RFUNCT_2:42
  Y c= dom h & h.:Y is bounded & upper_bound (h.:Y) = lower_bound (h.:Y)
implies h is_constant_on Y;

definition let h,Y;
pred h is_increasing_on Y means
:: RFUNCT_2:def 2
 for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r1 < h.r2;
pred h is_decreasing_on Y means
:: RFUNCT_2:def 3
 for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r2 < h.r1;
pred h is_non_decreasing_on Y means
:: RFUNCT_2:def 4
 for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r1 <= h.r2;
pred h is_non_increasing_on Y means
:: RFUNCT_2:def 5
 for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h & r1<r2 holds h.r2 <= h.r1;
end;

definition let h,Y;
pred h is_monotone_on Y means
:: RFUNCT_2:def 6
 h is_non_decreasing_on Y or h is_non_increasing_on Y;
end;

canceled 5;

theorem :: RFUNCT_2:48
h is_non_decreasing_on Y iff for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h &
  r1<=r2 holds h.r1 <= h.r2;

theorem :: RFUNCT_2:49
h is_non_increasing_on Y iff for r1,r2 st r1 in Y /\ dom h & r2 in Y /\ dom h &
  r1<=r2 holds h.r2 <= h.r1;

theorem :: RFUNCT_2:50
h is_increasing_on X iff h|X is_increasing_on X;

theorem :: RFUNCT_2:51
h is_decreasing_on X iff h|X is_decreasing_on X;

theorem :: RFUNCT_2:52
  h is_non_decreasing_on X iff h|X is_non_decreasing_on X;

theorem :: RFUNCT_2:53
  h is_non_increasing_on X iff h|X is_non_increasing_on X;

theorem :: RFUNCT_2:54
  Y misses dom h implies h is_increasing_on Y & h is_decreasing_on Y &
                      h is_non_decreasing_on Y & h is_non_increasing_on Y &
                      h is_monotone_on Y;

theorem :: RFUNCT_2:55
  h is_increasing_on Y implies h is_non_decreasing_on Y;

theorem :: RFUNCT_2:56
  h is_decreasing_on Y implies h is_non_increasing_on Y;

theorem :: RFUNCT_2:57
  h is_constant_on Y implies h is_non_decreasing_on Y;

theorem :: RFUNCT_2:58
  h is_constant_on Y implies h is_non_increasing_on Y;

theorem :: RFUNCT_2:59
  h is_non_decreasing_on Y & h is_non_increasing_on X implies
 h is_constant_on (Y /\ X);

theorem :: RFUNCT_2:60
  X c= Y & h is_increasing_on Y implies h is_increasing_on X;

theorem :: RFUNCT_2:61
  X c= Y & h is_decreasing_on Y implies h is_decreasing_on X;

theorem :: RFUNCT_2:62
  X c= Y & h is_non_decreasing_on Y implies h is_non_decreasing_on X;

theorem :: RFUNCT_2:63
  X c= Y & h is_non_increasing_on Y implies h is_non_increasing_on X;

theorem :: RFUNCT_2:64
(h is_increasing_on Y & 0<r implies r(#)h is_increasing_on Y) &
(r = 0 implies r(#)h is_constant_on Y) &
(h is_increasing_on Y & r<0 implies r(#)h is_decreasing_on Y);

theorem :: RFUNCT_2:65
  (h is_decreasing_on Y & 0<r implies r(#)h is_decreasing_on Y) &
(h is_decreasing_on Y & r<0 implies r(#)h is_increasing_on Y);

theorem :: RFUNCT_2:66
(h is_non_decreasing_on Y & 0<=r implies r(#)h is_non_decreasing_on Y) &
(h is_non_decreasing_on Y & r<=0 implies r(#)h is_non_increasing_on Y);

theorem :: RFUNCT_2:67
  (h is_non_increasing_on Y & 0<=r implies r(#)h is_non_increasing_on Y) &
(h is_non_increasing_on Y & r<=0 implies r(#)h is_non_decreasing_on Y);

theorem :: RFUNCT_2:68
r in X /\ Y /\ dom (h1+h2) implies r in X /\ dom h1 & r in Y /\ dom h2;

theorem :: RFUNCT_2:69
  (h1 is_increasing_on X & h2 is_increasing_on Y implies
                                h1+h2 is_increasing_on (X /\ Y)) &
(h1 is_decreasing_on X & h2 is_decreasing_on Y implies
                                h1+h2 is_decreasing_on (X /\ Y)) &
(h1 is_non_decreasing_on X & h2 is_non_decreasing_on Y implies
                                h1+h2 is_non_decreasing_on X /\ Y) &
(h1 is_non_increasing_on X & h2 is_non_increasing_on Y implies
                                h1+h2 is_non_increasing_on X /\ Y);

theorem :: RFUNCT_2:70
  (h1 is_increasing_on X & h2 is_constant_on Y implies
                               h1+h2 is_increasing_on X /\ Y) &
(h1 is_decreasing_on X & h2 is_constant_on Y implies
                               h1+h2 is_decreasing_on X /\ Y);

theorem :: RFUNCT_2:71
  h1 is_increasing_on X & h2 is_non_decreasing_on Y implies
 h1 + h2 is_increasing_on X /\ Y;

theorem :: RFUNCT_2:72
  h1 is_non_increasing_on X & h2 is_constant_on Y implies
 h1 + h2 is_non_increasing_on X /\ Y;

theorem :: RFUNCT_2:73
  h1 is_decreasing_on X & h2 is_non_increasing_on Y implies
 h1 + h2 is_decreasing_on X /\ Y;

theorem :: RFUNCT_2:74
  h1 is_non_decreasing_on X & h2 is_constant_on Y implies
 h1 + h2 is_non_decreasing_on X /\ Y;

theorem :: RFUNCT_2:75
  h is_increasing_on {x};

theorem :: RFUNCT_2:76
  h is_decreasing_on {x};

theorem :: RFUNCT_2:77
  h is_non_decreasing_on {x};

theorem :: RFUNCT_2:78
  h is_non_increasing_on {x};

theorem :: RFUNCT_2:79
  id R is_increasing_on R;

theorem :: RFUNCT_2:80
  h is_increasing_on X implies -h is_decreasing_on X;

theorem :: RFUNCT_2:81
  h is_non_decreasing_on X implies -h is_non_increasing_on X;

theorem :: RFUNCT_2:82
  (h is_increasing_on [.p,g.] or h is_decreasing_on [.p,g.])
implies h|[.p,g.] is one-to-one;

theorem :: RFUNCT_2:83
  for h being one-to-one PartFunc of REAL, REAL st h is_increasing_on [.p,g.]
 holds (h|[.p,g.])" is_increasing_on h.:[.p,g.];

theorem :: RFUNCT_2:84
   for h being one-to-one PartFunc of REAL, REAL st h is_decreasing_on [.p,g.]
  holds (h|[.p,g.])" is_decreasing_on h.:[.p,g.];