Iio_mul_Iic_subset' — Mathlib

English

For all a,b, the product Iio(a)·Iic(b) is contained in Iio(ab): Iio(a)·Iic(b) ⊆ Iio(ab).

Русский

Для любых a,b произведение Iio(a) и Iic(b) содержится в Iio(ab).

LaTeX

$$$$ Iio(a) \\cdot Iic(b) \\subseteq Iio(a b). $$$$

Lean4

@[to_additive Iio_add_Iic_subset]
theorem Iio_mul_Iic_subset' (a b : α) : Iio a * Iic b ⊆ Iio (a * b) :=
  by
  have := mulLeftMono_of_mulLeftStrictMono α
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_lt_mul_of_lt_of_le hya hzb

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