Ioc_mul_Ico_subset' — Mathlib

English

Let α be as above with Locally Finite Order. Then Ioc(a, b) · Ico(c, d) ⊆ Ioo(a c, b d).

Русский

Пусть α удовлетворяет тем же условиям. Тогда Ioc(a, b) · Ico(c, d) ⊆ Ioo(a c, b d).

LaTeX

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

Lean4

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

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