---

Step * of Lemma in-open-union

∀[X:Type]. ∀[x:X]. ∀[A:ℕ ⟶ Open(X)].  (x ∈ open-union(n.A[n]) ⇐⇒ ¬¬(∃n:ℕ. ((A[n] x) = ⊤ ∈ Sierpinski)))
BY
{ TACTIC:(Auto THEN All (RepUR ``Open in-open open-union``)) }

1
1. X : Type
2. x : X
3. A : ℕ ⟶ X ⟶ Sierpinski
4. lub(n.A[n] x) = ⊤ ∈ Sierpinski
⊢ ¬¬(∃n:ℕ. ((A[n] x) = ⊤ ∈ Sierpinski))

2
1. X : Type
2. x : X
3. A : ℕ ⟶ X ⟶ Sierpinski
4. ¬¬(∃n:ℕ. ((A[n] x) = ⊤ ∈ Sierpinski))
⊢ lub(n.A[n] x) = ⊤ ∈ Sierpinski

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[x:X].  \mforall{}[A:\mBbbN{}  {}\mrightarrow{}  Open(X)].    (x  \mmember{}  open-union(n.A[n])  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  ((A[n]  x)  =  \mtop{})))


By

---

Latex:
TACTIC:(Auto  THEN  All  (RepUR  ``Open  in-open  open-union``))

---

Home Index