Ico_mul_Ioc_subset'

Mathlib.Algebra.Group.Pointwise.Finset.Interval

URI: https://scilib.ai/kg/mathlib#Finset.Ico_mul_Ioc_subset'

← MathLib Explorer

English

Under the same hypotheses, Ico(a, b) · Ioc(c, d) ⊆ Ioo(a c, b d).

Русский

При тех же предпосылках Ico(a, b) · Ioc(c, d) ⊆ Ioo(a c, b d).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru