Nuprl Lemma : rat-cube-intersection-symm

[k:ℕ]. ∀[c,d:ℚCube(k)].  (c ⋂ d ⋂ c ∈ ℚCube(k))


Proof




Definitions occuring in Statement :  rat-cube-intersection: c ⋂ d rational-cube: Cube(k) nat: uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  nat: rat-cube-intersection: c ⋂ d rational-cube: Cube(k) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  int_seg_wf rat-interval-intersection-symm
Rules used in proof :  inhabitedIsType isectIsTypeImplies axiomEquality isect_memberEquality_alt because_Cache rename setElimination natural_numberEquality hypothesis hypothesisEquality applyEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule functionExtensionality cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c,d:\mBbbQ{}Cube(k)].    (c  \mcap{}  d  =  d  \mcap{}  c)



Date html generated: 2019_10_29-AM-07_51_18
Last ObjectModification: 2019_10_18-PM-00_48_55

Theory : rationals


Home Index