Icc_mul_Icc_subset' — Mathlib

English

For a ≤ b and c ≤ d, the product of the closed intervals Icc(a,b) and Icc(c,d) equals the closed interval Icc(ac, bd): Icc(a,b)·Icc(c,d) = Icc(ac, bd).

Русский

Пусть a ≤ b и c ≤ d. Произведение замкнутых интервалов Icc(a,b) и Icc(c,d) равно Icc(ac, bd).

LaTeX

$$$$ Icc(a,b) \\cdot Icc(c,d) = Icc(a c, b d) \\\\text{ при } a \\le b,\\; c \\le d. $$$$

Lean4

@[to_additive Icc_add_Icc_subset]
theorem Icc_mul_Icc_subset' (a b c d : α) : Icc a b * Icc c d ⊆ Icc (a * c) (b * d) :=
  by
  rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩
  exact ⟨mul_le_mul' hya hzc, mul_le_mul' hyb hzd⟩

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