iccHomeoI_symm_apply_coe — Mathlib

English

Let a and b be elements of a ordered field with a < b. The inverse of the affine map that sends the unit interval [0,1] to the closed interval [a,b] acts by x ↦ (b − a) x + a on x ∈ [0,1].

Русский

Пусть a < b в упорядоченном полям; обратное линейное отображение, переводящее единичный интервал в замкнутый интервал [a,b], действует на x ∈ [0,1] как x ↦ (b − a) x + a.

LaTeX

$$$\\forall a,b\\in 𝕜\\, (h: a < b)\\,\\forall x\\in \\mathrm{Icc}(0,1):\\ ((iccHomeoI\,a\,b\,h).symm x : 𝕜) = (b - a) \\cdot x + a$,$$

Lean4

@[simp]
theorem iccHomeoI_symm_apply_coe (a b : 𝕜) (h : a < b) (x : Set.Icc (0 : 𝕜) (1 : 𝕜)) :
    ((iccHomeoI a b h).symm x : 𝕜) = (b - a) * x + a :=
  rfl

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