inf_div_right — Mathlib

English

Let α be a type, β a Semilattice with Inf and Top, s,t Finset α, f: α → β. Then inf (s / t) f equals inf over y ∈ t of inf over x ∈ s of f(x/y).

Русский

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

LaTeX

$$$$ \\inf (s / t) f = \\inf_{y \\in t} \\; \\inf_{x \\in s} f(x/y) $$$$

Lean4

@[to_additive]
theorem inf_div_right [SemilatticeInf β] [OrderTop β] (s t : Finset α) (f : α → β) :
    inf (s / t) f = inf t fun y ↦ inf s (f <| · / y) :=
  inf_image₂_right ..

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