Icc_mul_Icc_subset' — Mathlib

English

For a LocallyFiniteOrder α, the product of two intervals Icc a b and Icc c d is contained in Icc (a c) (b d): Icc a b · Icc c d ⊆ Icc (a c) (b d).

Русский

Для LocallyFiniteOrder α произведение двух интервалов Icc a b и Icc c d подлежит включению в Icc (a c) (b d).

LaTeX

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

Lean4

@[to_additive Icc_add_Icc_subset]
theorem Icc_mul_Icc_subset' [LocallyFiniteOrder α] (a b c d : α) : Icc a b * Icc c d ⊆ Icc (a * c) (b * d) :=
  Finset.coe_subset.mp <| by simpa using Set.Icc_mul_Icc_subset' _ _ _ _

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