Nuprl Lemma : rceq_wf

[k:ℕ]. ∀[a,b:ℚCube(k)].  (rceq(k;a;b) ∈ 𝔹)


Proof




Definitions occuring in Statement :  rceq: rceq(k;a;b) rational-cube: Cube(k) nat: bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  deq: EqDecider(T) subtype_rel: A ⊆B rceq: rceq(k;a;b) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  istype-nat rational-cube_wf rc-deq_wf
Rules used in proof :  universeIsType isectIsTypeImplies isect_memberEquality_alt axiomEquality equalitySymmetry equalityTransitivity inhabitedIsType rename setElimination lambdaEquality_alt hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid applyEquality sqequalRule cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[a,b:\mBbbQ{}Cube(k)].    (rceq(k;a;b)  \mmember{}  \mBbbB{})



Date html generated: 2019_10_29-AM-07_49_15
Last ObjectModification: 2019_10_28-AM-10_59_46

Theory : rationals


Home Index