affineHomeomorph_image_Ioo — Mathlib

English

If a > 0, the image of the open interval (c,d) under x ↦ a x + b is (a c + b, a d + b).

Русский

Если a > 0, образ открытого интервала (c,d) под x ↦ a x + b равен (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_Ioo {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b) := by simp [h]

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