image_affine_Ioc — Mathlib

English

If a > 0, the affine map x ↦ a x + b sends Ioo(c, d) to Ioo(a c + b, a d + b).

Русский

Если a > 0, аффинное отображение x ↦ a x + b переводит Ioo(c, d) в Ioo(a c + b, a d + b).

LaTeX

$$$ (a \cdot \cdot + b)'' Ioo(c, d) = Ioo(a c + b, a d + b) $$$

Lean4

@[simp]
theorem image_affine_Ioc (h : 0 < a) (b c d : K) : (a * · + b) '' Ioc c d = Ioc (a * c + b) (a * d + b) :=
  by
  suffices (· + b) '' ((a * ·) '' Ioc c d) = Ioc (a * c + b) (a * d + b) by rwa [Set.image_image] at this
  rw [image_mul_left_Ioc h, image_add_const_Ioc]

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