---

Step * of Lemma weak-continuity-principle-real-double

∀x:ℝ. ∀F,H:ℝ ⟶ 𝔹. ∀G:n:ℕ+ ⟶ {y:ℝ| x = y ∈ (ℕ+n ⟶ ℤ)} .  (∃n:{ℕ+| (F x = F (G n) ∧ H x = H (G n))})
BY
{ Auto }

1
1. x : ℝ
2. F : ℝ ⟶ 𝔹
3. H : ℝ ⟶ 𝔹
4. G : n:ℕ+ ⟶ {y:ℝ| x = y ∈ (ℕ+n ⟶ ℤ)} 
⊢ ∃n:{ℕ+| (F x = F (G n) ∧ H x = H (G n))}

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}F,H:\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{y:\mBbbR{}|  x  =  y\}  .    (\mexists{}n:\{\mBbbN{}\msupplus{}|  (F  x  =  F  (G  n)  \mwedge{}  H  x  =  H  (G  n))\})


By

---

Latex:
Auto

---

Home Index