---

Step * 1 1 1 2 1 2 1 of Lemma sp-lub-is-bottom


1. n : ℕ
2. EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
3. B : Base
4. B1 : Base
5. B ∈ f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)
⊢ istype(B ∈ ℕ ⟶ ℕ ⟶ 𝔹)
BY
{ (Thin (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  EquivRel(\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{};f,g.fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g))
3.  B  :  Base
4.  B1  :  Base
5.  B  \mmember{}  f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g)
\mvdash{}  istype(B  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{})


By

---

Latex:
(Thin  (-1)  THEN  Auto)

---

Home Index