sInf_image' — Mathlib

English

Let s be a set and f: β → α. Then the infimum of the image f''s equals the infimum over a ∈ s of f(a).

Русский

Пусть $s$ — множество и $f: \beta \to \alpha$. Тогда инфиму́мум образа $f''s$ равен инфиму́муму по $a \in s$ от $f(a)$.

LaTeX

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

Lean4

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

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