sInf_image — Mathlib

English

Let α be a complete lattice, β a type, s a subset of β, and f a function from β to α. Then the infimum of the image f''s equals the infimum over s of f.

Русский

Пусть α — полная решетка, β — множество, s ⊆ β, и f: β → α. Тогда инфиминум изображения равен инфиминуму по элементам s для f.

LaTeX

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

Lean4

theorem sInf_image {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a ∈ s, f a :=
  @sSup_image αᵒᵈ _ _ _ _

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