---

Step * of Lemma es-is-interface-filter

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[P:A ─→ 𝔹]. ∀[e:E].
  uiff(↑e ∈b X|a.P[a];{(↑e ∈b X) ∧ (↑P[X(e)])})
BY
{ RemoveUniform Auto Auto }

1
∀Info:Type. ∀es:EO+(Info). ∀A:Type. ∀X:EClass(A). ∀P:A ─→ 𝔹. ∀e:E.  (↑e ∈b X|a.P[a] ⇐⇒ {(↑e ∈b X) ∧ (↑P[X(e)])})

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  X|a.P[a];\{(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}P[X(e)])\})


By

---

Latex:
RemoveUniform  Auto  Auto

---

Home Index