sup_div_left — Mathlib

English

Let α be a type, β a Semilattice with top, s,t Finset α, f: α → β. Then sup (s / t) f equals sup over x ∈ s of the inner sup over y ∈ t of f(x/y).

Русский

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

LaTeX

$$$$ \\sup (s / t) f = \\sup_{x \\in s} \\bigl( \\sup_{y \\in t} f(x/y) \\bigr) $$$$

Lean4

@[to_additive]
theorem sup_div_left [SemilatticeSup β] [OrderBot β] (s t : Finset α) (f : α → β) :
    sup (s / t) f = sup s fun x ↦ sup t (f <| x / ·) :=
  sup_image₂_left ..

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