image_mul_right_Icc — Mathlib

English

If a ≤ b and c ≥ 0, then the image of Icc(a,b) under right multiplication by c is Icc(a c, b c).

Русский

Если a ≤ b и c ≥ 0, то образ Icc(a,b) при правом умножении на c есть Icc(ac, bc).

LaTeX

$$$(a \le b \land 0 \le c) \Rightarrow (\{ x c \mid x \in [a,b] \} = [a c, b c])$$$

Lean4

theorem image_mul_right_Icc (hab : a ≤ b) (hc : 0 ≤ c) : (· * c) '' Icc a b = Icc (a * c) (b * c) :=
  by
  cases eq_or_lt_of_le hc
  · subst c
    simp [(nonempty_Icc.2 hab).image_const]
  exact image_mul_right_Icc' a b ‹0 < c›

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