English
Under the conjugating homeomorphism, the coordinate of an interval element is given by (x − a)/(b − a).
Русский
Под сопряжённым гомоморфизмом координата элемента интервала равна (x − a)/(b − a).
LaTeX
$$iccHomeoI_apply_coe (a b : 𝕜) (h : a < b) (x : Set.Icc a b) : ((iccHomeoI a b h) x : 𝕜) = (x - a) / (b - a)$$
Lean4
/-- The affine homeomorphism from a nontrivial interval `[a,b]` to `[0,1]`.
-/
def iccHomeoI (a b : 𝕜) (h : a < b) : Set.Icc a b ≃ₜ Set.Icc (0 : 𝕜) (1 : 𝕜) :=
by
let e := Homeomorph.image (affineHomeomorph (b - a) a (sub_pos.mpr h).ne.symm) (Set.Icc 0 1)
refine (e.trans ?_).symm
apply Homeomorph.setCongr
rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]
simp
