---

Step * 1 1 2 of Lemma weak-overt-implies-overt


1. X : Type
2. ∀[Y:Type]. ∃f:Open(X × Y) ⟶ Open(Y). ∀A:Open(X × Y). ∀y:Y.  (y ∈ f A ⇐⇒ ¬¬(∃x:X. <x, y> ∈ A))
3. Y : Type
4. f : Open(X × Y) ⟶ Open(Y)
5. ∀A:Open(X × Y). ∀y:Y.  ((f A y) = ⊤ ∈ Sierpinski ⇐⇒ ¬¬(∃x:X. ((A <x, y>) = ⊤ ∈ Sierpinski)))
6. A : Open(X × Y)@i
7. B : Open(Y)@i
8. ∀x:X. ∀y:Y.  (((A <x, y>) = ⊤ ∈ Sierpinski) ⇒ ((B y) = ⊤ ∈ Sierpinski))
9. y : Y@i
10. (f A y) = ⊤ ∈ Sierpinski
⊢ (B y) = ⊤ ∈ Sierpinski
BY
{ TACTIC:((InstHyp [⌜A⌝;⌜y⌝] 5⋅ THENA Auto) THEN ThinTrivial) }

1
1. X : Type
2. ∀[Y:Type]. ∃f:Open(X × Y) ⟶ Open(Y). ∀A:Open(X × Y). ∀y:Y.  (y ∈ f A ⇐⇒ ¬¬(∃x:X. <x, y> ∈ A))
3. Y : Type
4. f : Open(X × Y) ⟶ Open(Y)
5. ∀A:Open(X × Y). ∀y:Y.  ((f A y) = ⊤ ∈ Sierpinski ⇐⇒ ¬¬(∃x:X. ((A <x, y>) = ⊤ ∈ Sierpinski)))
6. A : Open(X × Y)@i
7. B : Open(Y)@i
8. ∀x:X. ∀y:Y.  (((A <x, y>) = ⊤ ∈ Sierpinski) ⇒ ((B y) = ⊤ ∈ Sierpinski))
9. y : Y@i
10. (f A y) = ⊤ ∈ Sierpinski
11. ((f A y) = ⊤ ∈ Sierpinski) ⇐ ¬¬(∃x:X. ((A <x, y>) = ⊤ ∈ Sierpinski))
12. ¬¬(∃x:X. ((A <x, y>) = ⊤ ∈ Sierpinski))
⊢ (B y) = ⊤ ∈ Sierpinski

---

Latex:

---

Latex:

1.  X  :  Type
2.  \mforall{}[Y:Type].  \mexists{}f:Open(X  \mtimes{}  Y)  {}\mrightarrow{}  Open(Y).  \mforall{}A:Open(X  \mtimes{}  Y).  \mforall{}y:Y.    (y  \mmember{}  f  A  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}(\mexists{}x:X.  <x,  y>  \mmember{}  A))
3.  Y  :  Type
4.  f  :  Open(X  \mtimes{}  Y)  {}\mrightarrow{}  Open(Y)
5.  \mforall{}A:Open(X  \mtimes{}  Y).  \mforall{}y:Y.    ((f  A  y)  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}(\mexists{}x:X.  ((A  <x,  y>)  =  \mtop{})))
6.  A  :  Open(X  \mtimes{}  Y)@i
7.  B  :  Open(Y)@i
8.  \mforall{}x:X.  \mforall{}y:Y.    (((A  <x,  y>)  =  \mtop{})  {}\mRightarrow{}  ((B  y)  =  \mtop{}))
9.  y  :  Y@i
10.  (f  A  y)  =  \mtop{}
\mvdash{}  (B  y)  =  \mtop{}


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  5\mcdot{}  THENA  Auto)  THEN  ThinTrivial)

---

Home Index