Nuprl Lemma : rat-interval-intersection-symm
∀[I,J:ℚInterval]. (I ⋂ J = J ⋂ I ∈ ℚInterval)
Proof
Definitions occuring in Statement :
rat-interval-intersection: I ⋂ J,
rational-interval: ℚInterval,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
guard: {T},
uimplies: b supposing a,
subtype_rel: A ⊆r B,
true: True,
squash: ↓T,
rat-interval-intersection: I ⋂ J,
rational-interval: ℚInterval,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
subtype_rel_self,
int-subtype-rationals,
qmul_wf,
iff_weakening_equal,
qmin-as-qmax,
qmin_wf,
rationals_wf,
equal_wf,
qmax-symmetry
Rules used in proof :
inhabitedIsType,
isectIsTypeImplies,
axiomEquality,
isect_memberEquality_alt,
minusEquality,
independent_functionElimination,
independent_isectElimination,
equalitySymmetry,
equalityTransitivity,
baseClosed,
imageMemberEquality,
natural_numberEquality,
because_Cache,
imageElimination,
lambdaEquality_alt,
applyEquality,
hypothesis,
hypothesisEquality,
isectElimination,
extract_by_obid,
independent_pairEquality,
sqequalRule,
thin,
productElimination,
sqequalHypSubstitution,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[I,J:\mBbbQ{}Interval]. (I \mcap{} J = J \mcap{} I)
Date html generated:
2019_10_29-AM-07_48_26
Last ObjectModification:
2019_10_18-PM-00_48_37
Theory : rationals
Home
Index