---

Step * 1 of Lemma no-real-separation


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
BY
{ ((DistinguishCases ⌜∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y)))⌝⋅ THENA Auto) THEN ExRepD) }

1
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x1 : ℝ
5. A[x1]
6. y1 : ℝ
7. B[y1]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. x : ℝ
10. y : ℝ
11. x = y
12. ↑isl(d x)
13. ↑isr(d y)
⊢ False

2
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x : ℝ
5. A[x]
6. y : ℝ
7. B[y]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. ¬(∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y))))
⊢ False

---

Latex:

---

Latex:

1.  A  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  B  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  real-disjoint(x.A[x];y.B[y])
4.  \mexists{}x:\mBbbR{}.  A[x]
5.  \mexists{}y:\mBbbR{}.  B[y]
6.  d  :  r:\mBbbR{}  {}\mrightarrow{}  (A[r]  +  B[r])
\mvdash{}  False


By

---

Latex:
((DistinguishCases  \mkleeneopen{}\mexists{}x,y:\mBbbR{}.  ((x  =  y)  \mwedge{}  (\muparrow{}isl(d  x))  \mwedge{}  (\muparrow{}isr(d  y)))\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index