---

Step * of Lemma inhabited-covers-real-implies

∀[A,B:ℝ ⟶ ℙ].
  ((∃a:ℝ. A[a])
  ⇒ (∃b:ℝ. B[b])
  ⇒ (∀r:ℝ. (A[r] ∨ B[r]))
  ⇒ (∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)))
BY
{ (Auto THEN RenameVar `d' (-1) THEN RepUR ``all or`` -1 THEN ExRepD) }

1
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. d : r:ℝ ⟶ (A[r] + B[r])
⊢ ∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)

---

Latex:

---

Latex:
\mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}a:\mBbbR{}.  A[a])
    {}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  B[b])
    {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r]))
    {}\mRightarrow{}  (\mexists{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mexists{}x:\mBbbR{}.  ((\mforall{}n:\mBbbN{}.  A[f  n])  \mwedge{}  (\mforall{}n:\mBbbN{}.  B[g  n])  \mwedge{}  lim  n\mrightarrow{}\minfty{}.f  n  =  x  \mwedge{}  lim  n\mrightarrow{}\minfty{}.g  n  =  x)))


By

---

Latex:
(Auto  THEN  RenameVar  `d'  (-1)  THEN  RepUR  ``all  or``  -1  THEN  ExRepD)

---

Home Index