---

Step * 1 of Lemma fun-ss-eq


1. ss : SeparationSpace
2. A : Type
3. f : A ⟶ Point(ss)
4. g : A ⟶ Point(ss)
5. ∀a:A. (¬f a # g a)
⊢ ¬(∃a:A. f a # g a)
BY
{ ((D 0 THENA Auto) THEN D -1) }

1
1. ss : SeparationSpace
2. A : Type
3. f : A ⟶ Point(ss)
4. g : A ⟶ Point(ss)
5. ∀a:A. (¬f a # g a)
6. a : A
7. f a # g a
⊢ False

---

Latex:

---

Latex:

1.  ss  :  SeparationSpace
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  Point(ss)
4.  g  :  A  {}\mrightarrow{}  Point(ss)
5.  \mforall{}a:A.  (\mneg{}f  a  \#  g  a)
\mvdash{}  \mneg{}(\mexists{}a:A.  f  a  \#  g  a)


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1)

---

Home Index