sup_div_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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