---

Step * of Lemma not-proj-sep-iff-proj-eq

No Annotations
∀n:ℕ. ∀a,b:ℙ^n.  (¬a ≠ b ⇐⇒ a = b)
BY
{ Auto }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ¬a ≠ b
⊢ a = b

2
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. a = b
⊢ ¬a ≠ b

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbP{}\^{}n.    (\mneg{}a  \mneq{}  b  \mLeftarrow{}{}\mRightarrow{}  a  =  b)


By

---

Latex:
Auto

---

Home Index