Nuprl Lemma : m-sup-property1

[X:Type]
  ∀d:metric(X). ∀mtb:m-TB(X;d). ∀f:X ⟶ ℝ. ∀mc:UC(f:X ⟶ ℝ).  sup(λr.∃x:X. (r (f x))) m-sup{i:l}(d;mtb;f;mc)


Proof




Definitions occuring in Statement :  m-sup: m-sup{i:l}(d;mtb;f;mc) m-TB: m-TB(X;d) m-unif-cont: UC(f:X ⟶ Y) rmetric: rmetric() metric: metric(X) sup: sup(A) b req: y real: uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  pi1: fst(t) pi2: snd(t) uimplies: supposing a guard: {T} rset: Set(ℝ) exists: x:A. B[x] and: P ∧ Q prop: subtype_rel: A ⊆B implies:  Q member: t ∈ T m-sup: m-sup{i:l}(d;mtb;f;mc) all: x:A. B[x] uall: [x:A]. B[x]
Lemmas referenced :  istype-universe sup_wf subtype_rel_self req_transitivity req_inversion req_wf inf_wf rmetric_wf m-unif-cont_wf real_wf m-TB_wf metric_wf m-TB-sup-and-inf
Rules used in proof :  universeEquality independent_functionElimination dependent_functionElimination equalityIstype functionEquality functionExtensionality because_Cache independent_isectElimination dependent_pairFormation_alt productElimination productEquality dependent_set_memberEquality_alt productIsType sqequalHypSubstitution introduction universeIsType functionIsType isectIsType equalitySymmetry equalityTransitivity isectElimination lambdaEquality_alt sqequalRule applyEquality hypothesisEquality inhabitedIsType hypothesis extract_by_obid instantiate thin cut lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}mtb:m-TB(X;d).  \mforall{}f:X  {}\mrightarrow{}  \mBbbR{}.  \mforall{}mc:UC(f:X  {}\mrightarrow{}  \mBbbR{}).
        sup(\mlambda{}r.\mexists{}x:X.  (r  =  (f  x)))  =  m-sup\{i:l\}(d;mtb;f;mc)



Date html generated: 2019_10_30-AM-06_54_44
Last ObjectModification: 2019_10_25-PM-02_22_02

Theory : reals


Home Index