sup_singleton_apply — Mathlib

English

For any Finset β and function f: β → α, the supremum of the family consisting of singletons {f(b)} over b ∈ β equals the image of f: (s.sup (λ b, {f(b)})) = image f.

Русский

Для любого Finset β и функции f: β → α, супремум семейства единственных множеств {f(b)} по b ∈ β равен образу f: (s.sup (λ b, {f(b)})) = image f.

LaTeX

$$$\\mathrm{sup}\\_{b\\in s} \\{f(b)\\} = s.\\mathrm{image} f$$$

Lean4

@[simp]
theorem sup_singleton_apply (s : Finset β) (f : β → α) : (s.sup fun b => {f b}) = s.image f :=
  by
  ext a
  rw [mem_sup, mem_image]
  simp only [mem_singleton, eq_comm]

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