coe_inf_of_nonempty — Mathlib

English

Let s be nonempty finite subset of β and f: β → α. The infimum over f corresponds to the infimum over the coerced function into WithTop α: (↑(s.inf f) ) = s.inf (↑ ∘ f).

Русский

Пусть s — непустое конечное подмножество β и f: β → α. Инфинум по f эквивалентен инфинуму по коэрцированной функции в WithTop α: ↑(inf f) = inf (↑ ∘ f).

LaTeX

$$$s \neq \varnothing \Rightarrow \uparrow\bigl(\inf_{x \in s} f(x)\bigr) = \inf_{x \in s} \uparrow f(x) \quad \text{в } \mathrm{WithTop}\,\alpha$$$

Lean4

theorem coe_inf_of_nonempty {s : Finset β} (h : s.Nonempty) (f : β → α) : (↑(s.inf f) : WithTop α) = s.inf ((↑) ∘ f) :=
  coe_sup_of_nonempty (α := αᵒᵈ) h f

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