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