affineHomeomorph_image_Ico — Mathlib

English

If a > 0, the affine map x ↦ a x + b sends the half-open interval [c,d) onto [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_Ico {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b) := by simp [h]

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