Nuprl Lemma : closed-rational-interval_wf
∀[a:ℤ]. ∀[b:ℤ-o]. ∀[c:ℤ]. ∀[d:ℤ-o]. (closed-rational-interval(a;b;c;d) ∈ Interval)
Proof
Definitions occuring in Statement :
closed-rational-interval: closed-rational-interval(a;b;c;d),
interval: Interval,
int_nzero: ℤ-o,
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
closed-rational-interval: closed-rational-interval(a;b;c;d)
Lemmas referenced :
rccint_wf,
rat-to-real_wf,
int_nzero_wf,
istype-int
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
inhabitedIsType,
isect_memberEquality_alt,
isectIsTypeImplies,
universeIsType
Latex:
\mforall{}[a:\mBbbZ{}]. \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}]. \mforall{}[c:\mBbbZ{}]. \mforall{}[d:\mBbbZ{}\msupminus{}\msupzero{}]. (closed-rational-interval(a;b;c;d) \mmember{} Interval)
Date html generated:
2019_10_29-AM-10_46_00
Last ObjectModification:
2019_10_16-AM-09_12_08
Theory : reals
Home
Index