Iic_mul_Iio_subset' — Mathlib

English

If α has a bottom element and Locally Finite Order with bot, then Iic(a) · Iio(b) ⊆ Iio(a b).

Русский

Пусть α имеет нижнюю границу и локальный конечный порядок с нулём, тогда Iic(a) · Iio(b) ⊆ Iio(a b).

LaTeX

$$$ Iic(a) \cdot Iio(b) \subseteq Iio(ab) $$$

Lean4

@[to_additive Iic_add_Iio_subset]
theorem Iic_mul_Iio_subset' [LocallyFiniteOrderBot α] (a b : α) : Iic a * Iio b ⊆ Iio (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Iic_mul_Iio_subset' _ _

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