Ico_mul_Ioc_subset' — Mathlib

English

For all a,b,c,d, the product Ioc(a,b)·Icc(c,d) is contained in Ioo(ac,bd): Ioc(a,b)·Icc(c,d) ⊆ Ioo(ac,bd).

Русский

Для любых a,b,c,d произведение Ioc(a,b) и Icc(c,d) содержится в Ioo(ac,bd).

LaTeX

$$$$ Ioc(a,b) \\cdot Icc(c,d) \\subseteq Ioo(a c, b d). $$$$

Lean4

@[to_additive Ico_add_Ioc_subset]
theorem Ico_mul_Ioc_subset' (a b c d : α) : Ico a b * Ioc c d ⊆ Ioo (a * c) (b * d) :=
  by
  have := mulLeftMono_of_mulLeftStrictMono α
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_lt_mul_of_le_of_lt hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

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