Ici_mul_Ici_subset' — Mathlib

English

In a locally finite order with a top element, and with multiplication monotone, for all a, b ∈ α, the product of upper sets Ici a and Ici b is contained in Ici (a b).

Русский

В локально конечном порядке с верхним элементом и монотонным умножением для любых a, b ∈ α произведение верхних множеств Ici a и Ici b содержится в Ici (a b).

LaTeX

$$$Ici(a) * Ici(b) \subseteq Ici(a b)$$$

Lean4

@[to_additive Ici_add_Ici_subset]
theorem Ici_mul_Ici_subset' [LocallyFiniteOrderTop α] (a b : α) : Ici a * Ici b ⊆ Ici (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Ici_mul_Ici_subset' _ _

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