---

Step * of Lemma weak-overt-implies-overt

∀[X:Type]. (wOvert(X) ⇒ Overt(X))
BY
{ TACTIC:(Auto THEN All (Unfolds ``weak-overt overt``) THEN RepeatFor 2 (ParallelLast) THEN (UnivCD THENA Auto)) }

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.  (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

---

Latex:

---

Latex:
\mforall{}[X:Type].  (wOvert(X)  {}\mRightarrow{}  Overt(X))


By

---

Latex:
TACTIC:(Auto
                THEN  All  (Unfolds  ``weak-overt  overt``)
                THEN  RepeatFor  2  (ParallelLast)
                THEN  (UnivCD  THENA  Auto))

---

Home Index