Nuprl Lemma : i-type-member
∀I:Interval. ∀p:i-type(I). (real(p) ∈ I)
Proof
Definitions occuring in Statement :
i-real: real(p),
i-type: i-type(I),
i-member: r ∈ I,
interval: Interval,
all: ∀x:A. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
i-type: i-type(I),
i-real: real(p),
pi2: snd(t),
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
exists: ∃x:A. B[x],
uall: ∀[x:A]. B[x],
sq_stable: SqStable(P),
squash: ↓T,
prop: ℙ
Lemmas referenced :
interval_wf,
i-type_wf,
i-member_wf,
i-approx_wf,
sq_stable__i-member,
i-member-iff
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
sqequalRule,
cut,
lemma_by_obid,
dependent_functionElimination,
hypothesisEquality,
setElimination,
rename,
independent_functionElimination,
dependent_pairFormation,
isectElimination,
hypothesis,
introduction,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
\mforall{}I:Interval. \mforall{}p:i-type(I). (real(p) \mmember{} I)
Date html generated:
2016_05_18-AM-08_48_52
Last ObjectModification:
2016_01_17-AM-02_25_46
Theory : reals
Home
Index