---

Step * of Lemma cut-of-closed

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[s:fset(E(X))]. ∀[e:E(X)].
  f e ∈ cut(X;f;s) ∧ prior(X)(e) ∈ cut(X;f;s) supposing ↑e ∈b prior(X) ∧ e ∈ cut(X;f;s) supposing e ∈ s
BY
{ RemoveUniform Auto Auto }

1
∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀s:fset(E(X)). ∀e:E(X).
  (e ∈ s ⇒ (f e ∈ cut(X;f;s) ∧ prior(X)(e) ∈ cut(X;f;s) supposing ↑e ∈b prior(X) ∧ e ∈ cut(X;f;s)))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[s:fset(E(X))].
\mforall{}[e:E(X)].
    f  e  \mmember{}  cut(X;f;s)  \mwedge{}  prior(X)(e)  \mmember{}  cut(X;f;s)  supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)  \mwedge{}  e  \mmember{}  cut(X;f;s) 
    supposing  e  \mmember{}  s


By

---

Latex:
RemoveUniform  Auto  Auto

---

Home Index