inf_eq_sInf_image — Mathlib

English

In a complete lattice β, for a finite set s and a function f : α → β, the infimum over s of f equals the infimum of the image f''s; i.e., inf_{a ∈ s} f(a) = inf (f'' s).

Русский

В полной решётке β для конечного множества s и отображения f: α → β инфимум по s равен инфимуму образа f(s).

LaTeX

$$$\inf_{a \in s} f(a) = \inf (f'' s)$$$

Lean4

theorem inf_eq_sInf_image [CompleteLattice β] (s : Finset α) (f : α → β) : s.inf f = sInf (f '' s) :=
  sup_eq_sSup_image (β := βᵒᵈ) ..

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