Ioc_mul_Ico_subset' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive Ioc_add_Ico_subset]
theorem Ioc_mul_Ico_subset' (a b c d : α) : Ioc a b * Ico 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_lt_of_le hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

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