Nuprl Lemma : rmaximum-split

[n,m:ℤ]. ∀[x:{n..m 1-} ⟶ ℝ]. ∀[k:ℤ].
  (rmaximum(n;m;i.x[i]) rmax(rmaximum(n;k;i.x[i]);rmaximum(k 1;m;i.x[i]))) supposing (k < and (n ≤ k))


Proof




Definitions occuring in Statement :  rmaximum: rmaximum(n;m;k.x[k]) rmax: rmax(x;y) req: y real: int_seg: {i..j-} less_than: a < b uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] le: A ≤ B function: x:A ⟶ B[x] add: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a rmaximum: rmaximum(n;m;k.x[k]) nat: all: x:A. B[x] decidable: Dec(P) or: P ∨ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False and: P ∧ Q prop: guard: {T} ge: i ≥  sq_type: SQType(T) subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than: a < b squash: T less_than': less_than'(a;b) uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) cand: c∧ B iff: ⇐⇒ Q rev_implies:  Q subtract: m true: True bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[k:\mBbbZ{}].
    (rmaximum(n;m;i.x[i])  =  rmax(rmaximum(n;k;i.x[i]);rmaximum(k  +  1;m;i.x[i])))  supposing 
          (k  <  m  and 
          (n  \mleq{}  k))



Date html generated: 2020_05_20-AM-11_14_11
Last ObjectModification: 2019_12_14-PM-00_56_15

Theory : reals


Home Index