Iic_mul_Iic_subset' — Mathlib

English

Let (α, ≤, ⋅) be a partially ordered set with a monotone multiplication in each argument and locally finite order with a bottom element. Then for all a, b ∈ α, and all x ≤ a, y ≤ b, one has x ⋅ y ≤ a ⋅ b.

Русский

Пусть (α, ≤, ⋅) — частично упорядоченное множество с монотонным умножением по каждому аргументу и локально конечным порядком с нулём. Тогда для любых a, b ∈ α и любых x ≤ a, y ≤ b выполняется x ⋅ y ≤ a ⋅ b.

LaTeX

$$$\{ x y \mid x \le a,\; y \le b \} \subseteq \{ z \mid z \le a b \}$$$

Lean4

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

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