Nuprl Lemma : decidable__equal_rational-interval
∀I,J:ℚInterval. Dec(I = J ∈ ℚInterval)
Proof
Definitions occuring in Statement :
rational-interval: ℚInterval,
decidable: Dec(P),
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
implies: P ⇒ Q,
so_apply: x[s],
prop: ℙ,
so_lambda: λ2x.t[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
rational-interval: ℚInterval
Lemmas referenced :
decidable__equal_set,
decidable__equal_rationals,
qle_wf,
rationals_wf,
decidable__equal_product
Rules used in proof :
productIsType,
setIsType,
because_Cache,
inhabitedIsType,
dependent_functionElimination,
independent_functionElimination,
universeIsType,
hypothesisEquality,
setEquality,
lambdaEquality_alt,
sqequalRule,
hypothesis,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}I,J:\mBbbQ{}Interval. Dec(I = J)
Date html generated:
2019_10_29-AM-07_46_45
Last ObjectModification:
2019_10_19-AM-10_35_15
Theory : rationals
Home
Index