Nuprl Lemma : cdrng_properties

[r:CDRng]. IsEqFun(|r|;=b)


Proof




Definitions occuring in Statement :  cdrng: CDRng rng_eq: =b rng_car: |r| eqfun_p: IsEqFun(T;eq) uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T eqfun_p: IsEqFun(T;eq) uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a prop: infix_ap: y cdrng: CDRng crng: CRng rng: Rng implies:  Q sq_stable: SqStable(P) squash: T
Lemmas referenced :  sq_stable__eqfun_p cdrng_wf rng_car_wf equal_wf assert_witness rng_eq_wf assert_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality productElimination independent_pairEquality axiomEquality hypothesis lemma_by_obid applyEquality setElimination rename equalityTransitivity equalitySymmetry independent_functionElimination imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}[r:CDRng].  IsEqFun(|r|;=\msubb{})



Date html generated: 2016_05_15-PM-00_20_56
Last ObjectModification: 2016_01_15-AM-08_51_33

Theory : rings_1


Home Index