### Nuprl Lemma : omral_dom_inj

`∀g:OCMon. ∀r:CDRng. ∀k:|g|. ∀v:|r|.`
`  (dom(inj(k,v)) = if v =b 0 then 0{g↓oset} else mset_inj{g↓oset}(k) fi  ∈ FiniteSet{g↓oset})`

Proof

Definitions occuring in Statement :  omral_inj: `inj(k,v)` omral_dom: `dom(ps)` mset_inj: `mset_inj{s}(x)` finite_set: `FiniteSet{s}` null_mset: `0{s}` ifthenelse: `if b then t else f fi ` infix_ap: `x f y` all: `∀x:A. B[x]` equal: `s = t ∈ T` cdrng: `CDRng` rng_zero: `0` rng_eq: `=b` rng_car: `|r|` oset_of_ocmon: `g↓oset` ocmon: `OCMon` grp_car: `|g|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` ocmon: `OCMon` omon: `OMon` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` abmonoid: `AbMon` mon: `Mon` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` uimplies: `b supposing a` bfalse: `ff` infix_ap: `x f y` so_apply: `x[s]` cand: `A c∧ B` oset_of_ocmon: `g↓oset` dset_of_mon: `g↓set` set_car: `|p|` pi1: `fst(t)` add_grp_of_rng: `r↓+gp` grp_car: `|g|` grp_eq: `=b` pi2: `snd(t)` grp_id: `e` omral_inj: `inj(k,v)` omral_dom: `dom(ps)`
Lemmas referenced :  oal_dom_inj oset_of_ocmon_wf subtype_rel_sets abmonoid_wf ulinorder_wf grp_car_wf assert_wf infix_ap_wf bool_wf grp_le_wf equal_wf grp_eq_wf eqtt_to_assert cancel_wf grp_op_wf uall_wf monot_wf cdrng_is_abdmonoid cdrng_wf ocmon_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality applyEquality sqequalRule instantiate hypothesis because_Cache lambdaEquality productEquality setElimination rename cumulativity universeEquality functionEquality unionElimination equalityElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination setEquality independent_pairFormation

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.  \mforall{}k:|g|.  \mforall{}v:|r|.
(dom(inj(k,v))  =  if  v  =\msubb{}  0  then  0\{g\mdownarrow{}oset\}  else  mset\_inj\{g\mdownarrow{}oset\}(k)  fi  )

Date html generated: 2017_10_01-AM-10_05_21
Last ObjectModification: 2017_03_03-PM-01_11_22

Theory : polynom_3

Home Index