English
The one-dimensional topological simplex is homeomorphic to the unit interval I.
Русский
Одномерный топологический простейший гомеоморфен единичному интервалу I.
LaTeX
$$$(\\langle 1 \\rangle).toTopObj \\cong_{\\mathrm{top}} I$$$
Lean4
/-- The one-dimensional topological simplex is homeomorphic to the unit interval. -/
def toTopObjOneHomeo : ⦋1⦌.toTopObj ≃ₜ I
where
toFun f := ⟨f 0, (f 0).2, toTopObj_one_coe_add_coe_eq_one f ▸ le_add_of_nonneg_right (f 1).2⟩
invFun x := ⟨![toNNReal x, toNNReal (σ x)], show ∑ _, _ = _ by ext; simp [toType_apply, Finset.sum]⟩
left_inv f := by ext i; fin_cases i <;> simp [← toTopObj_one_coe_add_coe_eq_one f]
right_inv x := by simp
continuous_toFun := .subtype_mk (continuous_subtype_val.comp ((continuous_apply _).comp continuous_subtype_val)) _
continuous_invFun := .subtype_mk (continuous_pi fun i ↦ by fin_cases i <;> dsimp <;> fun_prop) _
