---

Step * of Lemma rn-ss_wf

No Annotations
∀[n:ℕ]. (sepℝ^n ∈ SeparationSpace)
BY
{ ProveWfLemma }

1
1. n : ℕ
⊢ λx,y. x ≠ y ∈ {s:ℝ^n ⟶ ℝ^n ⟶ ℙ| ∀x:ℝ^n. (¬(s x x))} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  (sep\mBbbR{}\^{}n  \mmember{}  SeparationSpace)


By

---

Latex:
ProveWfLemma

---

Home Index