Nuprl Lemma : real-ring_wf
real-ring() ∈ CRng
Proof
Definitions occuring in Statement :
real-ring: real-ring(),
member: t ∈ T,
crng: CRng
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
quotient: x,y:A//B[x; y],
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
crng: CRng,
rng: Rng,
real-ring: real-ring(),
rng_sig: RngSig,
subtype_rel: A ⊆r B,
ring_p: IsRing(T;plus;zero;neg;times;one),
rng_car: |r|,
pi1: fst(t),
rng_plus: +r,
pi2: snd(t),
rng_zero: 0,
rng_minus: -r,
rng_times: *,
rng_one: 1,
bilinear: BiLinear(T;pl;tm),
monoid_p: IsMonoid(T;op;id),
group_p: IsGroup(T;op;id;inv),
infix_ap: x f y,
ident: Ident(T;op;id),
assoc: Assoc(T;op),
inverse: Inverse(T;op;id;inv),
cand: A c∧ B,
req_int_terms: t1 ≡ t2,
false: False,
not: ¬A,
top: Top,
comm: Comm(T;op)
Lemmas referenced :
quotient_wf,
real_wf,
req_wf,
req-equiv,
quotient-member-eq,
radd_wf,
radd_functionality,
rmul_wf,
rmul_functionality,
rminus_wf,
req_functionality,
rminus_functionality,
req_weakening,
ring_p_wf,
rng_car_wf,
rng_plus_wf,
rng_zero_wf,
rng_minus_wf,
rng_times_wf,
rng_one_wf,
comm_wf,
bfalse_wf,
int-to-real_wf,
subtype_quotient,
it_wf,
bool_wf,
req-implies-req,
radd-rminus,
radd-rminus-both,
radd-assoc,
rsub_wf,
itermSubtract_wf,
itermVar_wf,
itermAdd_wf,
itermConstant_wf,
req-iff-rsub-is-0,
rmul-assoc,
itermMultiply_wf,
rmul-distrib1,
rmul-distrib2,
real_polynomial_null,
istype-int,
real_term_value_sub_lemma,
istype-void,
real_term_value_var_lemma,
real_term_value_add_lemma,
real_term_value_const_lemma,
real_term_value_mul_lemma,
rmul_comm
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality_alt,
pointwiseFunctionalityForEquality,
functionEquality,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
sqequalRule,
hypothesisEquality,
inhabitedIsType,
universeIsType,
independent_isectElimination,
because_Cache,
pertypeElimination,
promote_hyp,
productElimination,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
productIsType,
equalityIstype,
sqequalBase,
dependent_set_memberEquality_alt,
setElimination,
rename,
dependent_pairEquality_alt,
closedConclusion,
natural_numberEquality,
applyEquality,
inrEquality_alt,
functionIsType,
unionIsType,
isect_memberFormation_alt,
isect_memberEquality_alt,
axiomEquality,
isectIsTypeImplies,
independent_pairFormation,
independent_pairEquality,
approximateComputation,
int_eqEquality,
voidElimination
Latex:
real-ring() \mmember{} CRng
Date html generated:
2019_10_30-AM-08_09_47
Last ObjectModification:
2019_09_18-PM-04_19_00
Theory : reals
Home
Index