---

Step * 1 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.  (y ∈ f A ⇐⇒ ¬¬(∃x:X. <x, y> ∈ A))
6. A : Open(X × Y)@i
7. B : Open(Y)@i
⊢ ∀y:Y. f A y ≤ B y ⇐⇒ ∀x:X. ∀y:Y.  A <x, y> ≤ B y
BY
{ TACTIC:(RepUR ``in-open`` -3 THEN RepUR ``sp-le`` 0) }

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
⊢ ∀y:Y. (((f A y) = ⊤ ∈ Sierpinski) ⇒ ((B y) = ⊤ ∈ Sierpinski))
⇐⇒ ∀x:X. ∀y:Y.  (((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.    (y  \mmember{}  f  A  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}(\mexists{}x:X.  <x,  y>  \mmember{}  A))
6.  A  :  Open(X  \mtimes{}  Y)@i
7.  B  :  Open(Y)@i
\mvdash{}  \mforall{}y:Y.  f  A  y  \mleq{}  B  y  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:X.  \mforall{}y:Y.    A  <x,  y>  \mleq{}  B  y


By

---

Latex:
TACTIC:(RepUR  ``in-open``  -3  THEN  RepUR  ``sp-le``  0)

---

Home Index