image_mul_left_Ioo — Mathlib

English

Let a > 0 in an ordered group with zero. Then left multiplication by a maps the open interval Ioo(b, c) onto Ioo(a b, a c).

Русский

Пусть a > 0 в упорядоченной группе с нулём. Левое умножение на a отображает открытый интервал Ioo(b, c) в Ioo(a b, a c).

LaTeX

$$$ a \cdot Ioo(b,c) = Ioo(a b, a c) $$$

Lean4

theorem image_mul_left_Ioo (h : 0 < a) (b c : G₀) : (a * ·) '' Ioo b c = Ioo (a * b) (a * c) :=
  (OrderIso.mulLeft₀ a h).image_Ioo b c

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