sup_toFinset — Mathlib

English

For β with decidable equality, the supremum over s of a multiset-valued function corresponds to a supremum over Finset of the toFinset images.

Русский

Пусть β имеет детерминированное равенство. Тогда супремум над s для функции, возвращающей множество (multiset), равен супремуму над B Finset от соответствующих образов.

LaTeX

$$$ (s.\sup f).toFinset = s.\sup (\lambda x. (f x).toFinset) $$$

Lean4

@[simp]
theorem sup_toFinset {α β} [DecidableEq β] (s : Finset α) (f : α → Multiset β) :
    (s.sup f).toFinset = s.sup fun x => (f x).toFinset :=
  comp_sup_eq_sup_comp Multiset.toFinset toFinset_union rfl

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