Nuprl Lemma : inhabited-rat-interval_wf
∀[I:ℚInterval]. (Inhabited(I) ∈ 𝔹)
Proof
Definitions occuring in Statement :
inhabited-rat-interval: Inhabited(I),
rational-interval: ℚInterval,
bool: 𝔹,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
rational-interval: ℚInterval,
inhabited-rat-interval: Inhabited(I),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rational-interval_wf,
q_le_wf
Rules used in proof :
universeIsType,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
hypothesis,
isectElimination,
extract_by_obid,
hypothesisEquality,
independent_pairEquality,
thin,
productElimination,
sqequalHypSubstitution,
spreadEquality,
sqequalRule,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[I:\mBbbQ{}Interval]. (Inhabited(I) \mmember{} \mBbbB{})
Date html generated:
2019_10_29-AM-07_47_32
Last ObjectModification:
2019_10_17-PM-04_32_13
Theory : rationals
Home
Index