sup_singleton_eq_self — Mathlib

English

For any finite set s, the supremum over the constant mapping to singletons of f equals the original set: s.sup singleton = s.

Русский

Для любого конечного множества s супремум отображения в единичные множества равен самому множеству: s.sup singleton = s.

LaTeX

$$$s.\\mathrm{sup}\\ \\mathrm{singleton} = s$$$

Lean4

@[simp]
theorem sup_singleton_eq_self (s : Finset α) : s.sup singleton = s :=
  (s.sup_singleton_apply _).trans image_id

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