Icc_mul_Ico_subset' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive Icc_add_Ico_subset]
theorem Icc_mul_Ico_subset' (a b c d : α) : Icc a b * Ico 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_le_of_lt hyb hzd⟩

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