Nuprl Lemma : real-continuity-principle_wf

real-continuity-principle() ∈ ℙ


Proof




Definitions occuring in Statement :  real-continuity-principle: real-continuity-principle() prop: member: t ∈ T
Definitions unfolded in proof :  real-continuity-principle: real-continuity-principle() member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] label: ...$L... t rfun: I ⟶ℝ so_apply: x[s] prop:
Lemmas referenced :  all_wf interval_wf rfun_wf continuous_wf real_wf i-member_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality hypothesisEquality because_Cache applyEquality setEquality

Latex:
real-continuity-principle()  \mmember{}  \mBbbP{}



Date html generated: 2016_05_18-AM-10_52_04
Last ObjectModification: 2015_12_27-PM-10_44_24

Theory : reals


Home Index