English
The one-dimensional standard simplex in 𝕜 on Fin 2 is equivalent to the unit interval via an explicit equivalence.
Русский
Одномерный стандартный симплекс на Fin 2 эквивалентен единичному интервалу через явную эквивалентность.
LaTeX
$$$\mathrm{stdSimplexEquivIcc}_{\mathbb{k}} : \mathrm{stdSimplex}_{\mathbb{k}}(\mathrm{Fin}\,2) \simeq Icc(0,1)$$$
Lean4
/-- The standard one-dimensional simplex in `ℝ² = Fin 2 → ℝ`
is homeomorphic to the unit interval. -/
@[simps! -fullyApplied]
def stdSimplexHomeomorphUnitInterval : stdSimplex ℝ (Fin 2) ≃ₜ unitInterval
where
toEquiv := stdSimplexEquivIcc ℝ
continuous_toFun := .subtype_mk ((continuous_apply 1).comp continuous_subtype_val) _
continuous_invFun := by
apply Continuous.subtype_mk
exact (continuous_pi <| Fin.forall_fin_two.2 ⟨continuous_const.sub continuous_subtype_val, continuous_subtype_val⟩)
