---

Step * of Lemma no-real-separation

∀[A,B:ℝ ⟶ ℙ].  (¬real-separation(x.A[x];y.B[y]))
BY
{ (Auto THEN (D 0 THENA Auto) THEN RepeatFor 3 (D -1) THEN Unfolds ``all or`` -1 THEN RenameVar `d' (-1)) }

1
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. ∃x:ℝ. A[x]
5. ∃y:ℝ. B[y]
6. d : r:ℝ ⟶ (A[r] + B[r])
⊢ False

---

Latex:

---

Latex:
\mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].    (\mneg{}real-separation(x.A[x];y.B[y]))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  3  (D  -1)
  THEN  Unfolds  ``all  or``  -1
  THEN  RenameVar  `d'  (-1))

---

Home Index