---

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


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)
BY
{ ((Assert EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)) BY
          (BLemma `fun-equiv-rel` THEN Auto THEN BLemma `equiv_rel_squash`⋅ THEN Auto))
   THEN (GenConcl ⌜A = B ∈ (f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))⌝⋅ THENA Auto)
   THEN ThinVar `A'
   THEN Thin 2) }

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

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  Sierpinski
2.  n  :  \mBbbN{}
3.  (\mBbbN{}  {}\mrightarrow{}  (a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}//(a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{})))  \msubseteq{}r  (f,g:\mBbbN{}
          {}\mrightarrow{}  \mBbbN{}
          {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g))
\mvdash{}  (lub(n.A[n])  =  \mbot{})  {}\mRightarrow{}  (A[n]  =  \mbot{})


By

---

Latex:
((Assert  EquivRel(\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{};f,g.fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g))  BY
                (BLemma  `fun-equiv-rel`  THEN  Auto  THEN  BLemma  `equiv\_rel\_squash`\mcdot{}  THEN  Auto))
  THEN  (GenConcl  \mkleeneopen{}A  =  B\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `A'
  THEN  Thin  2)

---

Home Index