Nuprl Lemma : endpoints_wf
∀[I:Interval]. endpoints(I) ∈ ℝ × ℝ supposing i-finite(I)
Proof
Definitions occuring in Statement :
endpoints: endpoints(I),
i-finite: i-finite(I),
interval: Interval,
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T,
product: x:A × B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
endpoints: endpoints(I),
interval: Interval,
i-finite: i-finite(I),
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ
Lemmas referenced :
outl_wf,
real_wf,
top_wf,
equal_wf,
i-finite_wf,
interval_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
independent_pairEquality,
extract_by_obid,
isectElimination,
unionEquality,
hypothesis,
hypothesisEquality,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
lambdaFormation,
unionElimination,
dependent_functionElimination,
independent_functionElimination,
axiomEquality,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[I:Interval]. endpoints(I) \mmember{} \mBbbR{} \mtimes{} \mBbbR{} supposing i-finite(I)
Date html generated:
2019_10_29-AM-10_45_20
Last ObjectModification:
2018_08_21-PM-02_00_51
Theory : reals
Home
Index