---

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


1. A : ℕ ⟶ Sierpinski
2. lub(n.A[n]) = ⊥ ∈ Sierpinski
3. n : ℕ
⊢ A[n] = ⊥ ∈ Sierpinski
BY
{ (MoveToConcl (-2)
   THEN (InstLemma `quotient-function-subtype` [⌜ℕ⌝;⌜ℕ ⟶ 𝔹⌝;⌜λ2f g.f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)⌝]⋅ THENA Auto)
   ) }

1
1. A : ℕ ⟶ Sierpinski
2. n : ℕ
3. (ℕ ⟶ (a,b:ℕ ⟶ 𝔹//(a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹)))) ⊆r (f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹)
                                                                                                      ⇐⇒ b
                                                                                                          = ⊥
                                                                                                          ∈ (ℕ
                                                                                                            ⟶ 𝔹);f;g))
⊢ (lub(n.A[n]) = ⊥ ∈ Sierpinski) ⇒ (A[n] = ⊥ ∈ Sierpinski)

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  Sierpinski
2.  lub(n.A[n])  =  \mbot{}
3.  n  :  \mBbbN{}
\mvdash{}  A[n]  =  \mbot{}


By

---

Latex:
(MoveToConcl  (-2)
  THEN  (InstLemma  `quotient-function-subtype`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mBbbN{}  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f  g.f  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  g  =  \mbot{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index