sup_mul_le — Mathlib

English

For β a semilattice with top and bottom, the inequality sup (s * t) f ≤ a is equivalent to saying f(x*y) ≤ a for all x ∈ s, y ∈ t.

Русский

Пусть β — полузамкнутая вверх полная частично упорядоченная множ. верх, тогда sup (s * t) f ≤ a эквивалентно f(x*y) ≤ a для всех x ∈ s, y ∈ t.

LaTeX

$$Iff (inst_2.le ((instHMul.hMul s t).sup f) a)\n (∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a)$$

Lean4

@[to_additive (attr := simp (default + 1))]
theorem sup_mul_le {β} [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
    sup (s * t) f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a :=
  sup_image₂_le

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