Ico_mul_Icc_subset' — Mathlib

English

Let α be a multiplicative ordered set with locally finite order, and suppose a, b, c, d ∈ α. Then the set product of the interval Ico(a, b) with the interval Icc(c, d) is contained in the interval Ico(a c, b d): Ico(a, b) · Icc(c, d) ⊆ Ico(a c, b d).

Русский

Пусть α — упорядоченное моноидное множество с локально конечным порядком, и возьмём a, b, c, d ∈ α. Тогда произведение множест Ico(a, b) и Icc(c, d) принадлежит интервалу Ico(a c, b d): Ico(a, b) · Icc(c, d) ⊆ Ico(a c, b d).

LaTeX

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

Lean4

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

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