Ico_mul_Icc_subset' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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