Nuprl Lemma : qeq-wf
∀[r,s:ℚ]. (qeq(r;s) ∈ 𝔹)
Proof
Definitions occuring in Statement :
rationals: ℚ,
qeq: qeq(r;s),
bool: 𝔹,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
rationals: ℚ,
quotient: x,y:A//B[x; y],
and: P ∧ Q,
prop: ℙ,
uimplies: b supposing a,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
equiv_rel: EquivRel(T;x,y.E[x; y]),
trans: Trans(T;x,y.E[x; y]),
all: ∀x:A. B[x],
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
sym: Sym(T;x,y.E[x; y]),
sq_type: SQType(T),
guard: {T}
Lemmas referenced :
true_wf,
bool_subtype_base,
subtype_base_sq,
qeq-equiv,
eqtt_to_assert,
assert_wf,
iff_imp_equal_bool,
rationals_wf,
qeq_wf,
equal-wf-T-base,
int_nzero_wf,
b-union_wf,
equal-wf-base,
bool_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
pointwiseFunctionalityForEquality,
lemma_by_obid,
hypothesis,
sqequalRule,
pertypeElimination,
productElimination,
thin,
productEquality,
isectElimination,
intEquality,
hypothesisEquality,
because_Cache,
baseClosed,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
independent_isectElimination,
independent_pairFormation,
lambdaFormation,
dependent_functionElimination,
independent_functionElimination,
natural_numberEquality,
instantiate,
cumulativity
Latex:
\mforall{}[r,s:\mBbbQ{}]. (qeq(r;s) \mmember{} \mBbbB{})
Date html generated:
2016_05_15-PM-10_37_04
Last ObjectModification:
2016_01_16-PM-09_37_38
Theory : rationals
Home
Index