Icc_mul_Ico_subset' — Mathlib

English

Let α be a locally finite order. Then for all a, b, c, d ∈ α, we have Icc(a, b) ⋅ Ico(c, d) ⊆ Ico(a c, b d); that is, if x ∈ [a, b] and y ∈ [c, d), then x y ∈ [a c, b d).

Русский

Пусть α — локально конечный порядок. Тогда для любых a, b, c, d ∈ α верно Icc(a, b) ⋅ Ico(c, d) ⊆ Ico(a c, b d); то есть если x ∈ [a, b], y ∈ [c, d), то x y ∈ [a c, b d).

LaTeX

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

Lean4

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

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