affineHomeomorph_image_Ioc — 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_Ioc {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b) := by simp [h]

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