Nuprl Lemma : omral_minus_wf

g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|.  (--ps ∈ |omral(g;r)|)


Proof




Definitions occuring in Statement :  omral_minus: --ps omralist: omral(g;r) all: x:A. B[x] member: t ∈ T cdrng: CDRng ocmon: OCMon set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T omral_minus: --ps uall: [x:A]. B[x] subtype_rel: A ⊆B dset: DSet omralist: omral(g;r) oalist: oal(a;b) dset_set: dset_set mk_dset: mk_dset(T, eq) set_car: |p| pi1: fst(t) dset_list: List set_prod: s × t oset_of_ocmon: g↓oset dset_of_mon: g↓set add_grp_of_rng: r↓+gp grp_id: e pi2: snd(t) grp_car: |g| cdrng: CDRng abdgrp: AbDGrp crng: CRng rng_car: |r| grp_eq: =b rng_eq: =b abgrp: AbGrp grp: Group{i} mon: Mon prop: ocmon: OCMon omon: OMon so_lambda: λ2x.t[x] and: P ∧ Q abmonoid: AbMon so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt band: p ∧b q ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a bfalse: ff infix_ap: y so_apply: x[s] cand: c∧ B
Lemmas referenced :  set_car_wf omralist_wf dset_wf cdrng_wf ocmon_wf cdrng_properties add_grp_of_rng_wf_b eqfun_p_wf grp_car_wf grp_eq_wf oal_neg_wf2 dset_of_mon_wf2 subtype_rel_sets abmonoid_wf ulinorder_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution hypothesis introduction extract_by_obid isectElimination thin dependent_functionElimination hypothesisEquality applyEquality lambdaEquality setElimination rename sqequalRule dependent_set_memberEquality because_Cache instantiate productEquality cumulativity universeEquality functionEquality unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination setEquality independent_pairFormation

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}ps:|omral(g;r)|.    (--ps  \mmember{}  |omral(g;r)|)



Date html generated: 2017_10_01-AM-10_05_17
Last ObjectModification: 2017_03_03-PM-01_14_04

Theory : polynom_3


Home Index