sup_div_le — Mathlib

English

Let α be a type, β be a Semilattice with top, s,t Finset α, and f: α → β. Then sup (s / t) f ≤ a is equivalent to: for every x ∈ s and y ∈ t, f(x/y) ≤ a.

Русский

Пусть α — множество, β — полугруппа с максимумом, s,t — конечные множества, f: α → β. Тогда верхняя граница по делению удовлетворяет: sup (s/t) f ≤ a эквивалентно тому, что для всех x ∈ s и y ∈ t выполняется f(x/y) ≤ a.

LaTeX

$$$$ \\sup (s / t) f \\le a \\;\\iff\\; \\forall x \\in s, \\forall y \\in t,\\; f(x/y) \\le a $$$$

Lean4

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

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