coe_sup_of_nonempty — Mathlib

English

Let s be a nonempty finite subset of β and f: β → α. The coercion of the supremum equals the supremum of the coerced values: (↑(s.sup f) : WithBot α) = s.sup (↑ ∘ f).

Русский

Пусть s — непустое конечное подмножество β и f: β → α. Тогда переход наверх отображает верхнюю грань так: ↑(sup f) = sup (↑ ∘ f) в WithBot α.

LaTeX

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

Lean4

theorem coe_sup_of_nonempty {s : Finset β} (h : s.Nonempty) (f : β → α) : (↑(s.sup f) : WithBot α) = s.sup ((↑) ∘ f) :=
  by simp only [← sup'_eq_sup h, coe_sup' h]

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