---

Step * 1 1 of Lemma omral_dom_action


1. g : OCMon
2. r : CDRng
3. v : |r|
4. ps : |omral(g;r)|
⊢ ↑(fs-map(λk'.(k' * e), dom(ps)) ⊆b dom(ps))
BY
{ ((BLemma `mem_bsubmset` THENM RepD) THENA Auto) }

1
1. g : OCMon
2. r : CDRng
3. v : |r|
4. ps : |omral(g;r)|
5. x : |(g↓oset)|
6. ↑(x
∈b fs-map(λk'.(k' * e), dom(ps)))
⊢ ↑(x
∈b dom(ps))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  v  :  |r|
4.  ps  :  |omral(g;r)|
\mvdash{}  \muparrow{}(fs-map(\mlambda{}k'.(k'  *  e),  dom(ps))  \msubseteq{}\msubb{}  dom(ps))


By

---

Latex:
((BLemma  `mem\_bsubmset`  THENM  RepD)  THENA  Auto)

---

Home Index