---

Step * 1 1 of Lemma no-real-separation


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
BY
{ (Unfold `real-disjoint` 3 THEN (FHyp 3 [-3] THENA Auto) THEN D -1 THEN Auto) }

1
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. ∀x,y:ℝ.  ((x = y) ⇒ (¬(A[x] ∧ 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)
⊢ A[x]

2
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. ∀x,y:ℝ.  ((x = y) ⇒ (¬(A[x] ∧ 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)
14. A[x]
⊢ B[y]

---

Latex:

---

Latex:

1.  A  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  B  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  real-disjoint(x.A[x];y.B[y])
4.  x1  :  \mBbbR{}
5.  A[x1]
6.  y1  :  \mBbbR{}
7.  B[y1]
8.  d  :  r:\mBbbR{}  {}\mrightarrow{}  (A[r]  +  B[r])
9.  x  :  \mBbbR{}
10.  y  :  \mBbbR{}
11.  x  =  y
12.  \muparrow{}isl(d  x)
13.  \muparrow{}isr(d  y)
\mvdash{}  False


By

---

Latex:
(Unfold  `real-disjoint`  3  THEN  (FHyp  3  [-3]  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index