---

Step * 1 2 2 2 of Lemma eo-restrict_property


1. es : EO@i'
2. P : E ─→ 𝔹@i
3. e : es-base-E(es)
4. ¬↑(es-dom(es) e)
⊢ False ∈ Type
BY
{ Auto }

---

Latex:



1.  es  :  EO@i'
2.  P  :  E  {}\mrightarrow{}  \mBbbB{}@i
3.  e  :  es-base-E(es)
4.  \mneg{}\muparrow{}(es-dom(es)  e)
\mvdash{}  False  \mmember{}  Type


By

Auto

---

Home Index