inf_div_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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