Nuprl Lemma : m-sup_wf

[X:Type]. ∀[d:metric(X)]. ∀[mtb:m-TB(X;d)]. ∀[f:X ⟶ ℝ]. ∀[mc:UC(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) real: uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  top: Top 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 all: x:A. B[x] m-sup: m-sup{i:l}(d;mtb;f;mc) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  istype-universe istype-void pi1_wf_top 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 voidElimination isect_memberEquality_alt independent_pairEquality 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 lambdaFormation_alt inhabitedIsType hypothesis extract_by_obid instantiate thin cut 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{})].
    (m-sup\{i:l\}(d;mtb;f;mc)  \mmember{}  \mBbbR{})



Date html generated: 2019_10_30-AM-06_54_24
Last ObjectModification: 2019_10_25-PM-02_20_20

Theory : reals


Home Index