affineHomeomorph_image_I — Mathlib

English

The unit interval is homeomorphic to any nontrivial closed interval via an affine homeomorphism.

Русский

Единичный интервал гомоморфен к любому не тривиальному замкнутому интервалу через аффинное гомеморфное отображение.

LaTeX

$$iccHomeoI a b h : Set.Icc a b ≃ₜ Set.Icc 0 1$$

Lean4

/-- The image of `[0,1]` under the homeomorphism `fun x ↦ a * x + b` is `[b, a+b]`.
-/
theorem affineHomeomorph_image_I (a b : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne.symm '' Set.Icc 0 1 = Set.Icc b (a + b) := by simp [h]

Похожие утверждения