Nuprl Lemma : i-witness_wf

[I:Interval]. ∀[r:ℝ]. ∀[p:r ∈ I].  (i-witness(I;r;p) ∈ ℕ+)


Proof




Definitions occuring in Statement :  i-witness: i-witness(I;r;p) i-member: r ∈ I interval: Interval real: nat_plus: + uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  top: Top uimplies: supposing a exists: x:A. B[x] so_apply: x[s] prop: implies:  Q so_lambda: λ2x.t[x] all: x:A. B[x] subtype_rel: A ⊆B member: t ∈ T uall: [x:A]. B[x] i-witness: i-witness(I;r;p)
Lemmas referenced :  equal_wf pi1_wf_top subtype_rel_function i-approx_wf nat_plus_wf exists_wf i-member_wf real_wf all_wf interval_wf subtype_rel_self i-member-witness
Rules used in proof :  axiomEquality independent_functionElimination dependent_functionElimination equalitySymmetry equalityTransitivity voidEquality voidElimination isect_memberEquality independent_pairEquality productElimination lambdaFormation independent_isectElimination because_Cache hypothesisEquality lambdaEquality functionEquality isectElimination sqequalHypSubstitution hypothesis extract_by_obid instantiate thin applyEquality cut introduction isect_memberFormation computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

Latex:
\mforall{}[I:Interval].  \mforall{}[r:\mBbbR{}].  \mforall{}[p:r  \mmember{}  I].    (i-witness(I;r;p)  \mmember{}  \mBbbN{}\msupplus{})



Date html generated: 2018_05_22-PM-02_05_11
Last ObjectModification: 2018_05_21-AM-00_18_02

Theory : reals


Home Index