Nuprl Lemma : rminimum-constant

[n,m:ℤ].  ∀[x:{n..m 1-} ⟶ ℝ]. ∀[r:ℝ].  rminimum(n;m;i.x[i]) supposing ∀i:{n..m 1-}. (x[i] r) supposing n ≤ m


Proof




Definitions occuring in Statement :  rminimum: rminimum(n;m;k.x[k]) req: y real: int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] le: A ≤ B all: x:A. B[x] 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 rminimum: rminimum(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) le: A ≤ B less_than': less_than'(a;b) so_apply: x[s] int_seg: {i..j-} lelt: i ≤ j < k so_lambda: λ2x.t[x] top: Top bool: 𝔹 unit: Unit it: btrue: tt subtype_rel: A ⊆B uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff cand: c∧ B less_than: a < b squash: T iff: ⇐⇒ Q rev_implies:  Q subtract: m true: True rev_uimplies: rev_uimplies(P;Q)

Latex:
\mforall{}[n,m:\mBbbZ{}].
    \mforall{}[x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[r:\mBbbR{}].    rminimum(n;m;i.x[i])  =  r  supposing  \mforall{}i:\{n..m  +  1\msupminus{}\}.  (x[i]  =  r) 
    supposing  n  \mleq{}  m



Date html generated: 2020_05_20-AM-11_15_49
Last ObjectModification: 2020_01_06-PM-00_25_38

Theory : reals


Home Index