image_affine_Icc' — Mathlib

English

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

Русский

Аффинное отображение x ↦ a x + b отправляет замкнутый интервал Icc(c, d) в Icc(a c + b, a d + b) при a > 0.

LaTeX

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

Lean4

@[simp]
theorem image_affine_Icc' (h : 0 < a) (b c d : K) : (a * · + b) '' Icc c d = Icc (a * c + b) (a * d + b) :=
  by
  suffices (· + b) '' ((a * ·) '' Icc c d) = Icc (a * c + b) (a * d + b) by rwa [Set.image_image] at this
  rw [image_mul_left_Icc' h, image_add_const_Icc]

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