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]