foldr_sup_eq_sup_toFinset — Mathlib

English

For any list, folding with ⊔ from the right starting at ⊥ equals the supremum over the Finset representation of the list of the identity function.

Русский

Для любого списка сложение справа с верхним пределом даёт тот же супремум над множеством элементов списка.

LaTeX

$$$\displaystyle List.\foldr (\\, \\u2295 \\u22c3) \bot l = l.\toFinset.\sup id$$$

Lean4

theorem _root_.List.foldr_sup_eq_sup_toFinset [DecidableEq α] (l : List α) : l.foldr (· ⊔ ·) ⊥ = l.toFinset.sup id :=
  by
  rw [← coe_fold_r, ← Multiset.fold_dedup_idem, sup_def, ← List.toFinset_coe, toFinset_val, Multiset.map_id]
  rfl

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