affineHomeomorph_image_Icc — Mathlib

English

If a > 0, the affine map x ↦ a x + b sends the closed interval [c,d] onto the closed interval [a c + b, a d + b].

Русский

Если a > 0, отображение x ↦ a x + b отправляет замкнутый интервал [c,d] в замкнутый интервал [a c + b, a d + b].

LaTeX

$$$\{ a x + b \mid x \in [c,d] \} = [a c + b, a d + b]\quad (a > 0).$$$

Lean4

theorem affineHomeomorph_image_Icc {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b) := by simp [h]

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