Nuprl Lemma : qeq-equiv
EquivRel(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
Proof
Definitions occuring in Statement :
qeq: qeq(r;s),
equiv_rel: EquivRel(T;x,y.E[x; y]),
int_nzero: ℤ-o,
b-union: A ⋃ B,
btrue: tt,
bool: 𝔹,
product: x:A × B[x],
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
equiv_rel: EquivRel(T;x,y.E[x; y]),
and: P ∧ Q,
cand: A c∧ B
Lemmas referenced :
qeq-refl,
qeq-sym,
qeq-trans
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
independent_pairFormation,
cut,
lemma_by_obid,
hypothesis
Latex:
EquivRel(\mBbbZ{} \mcup{} (\mBbbZ{} \mtimes{} \mBbbZ{}\msupminus{}\msupzero{});r,s.qeq(r;s) = tt)
Date html generated:
2016_05_15-PM-10_36_48
Last ObjectModification:
2015_12_27-PM-08_01_11
Theory : rationals
Home
Index