foldr_inf_eq_inf_toFinset — Mathlib

English

For a list l, the right-fold of inf under top is equal to the infimum over the corresponding Finset of l, i.e., l.foldr (⊓) ⊤ = l.toFinset.inf id.

Русский

Для списка l правостепенный свертка по инфумуму вершины равен инфимууму соответствующего множества элементов: l.foldr (⊓) ⊤ = l.toFinset.inf id.

LaTeX

$$$ List.\\,foldr (\\\\lambda x_1 x_2, x_1 \\\\wedge x_2) \\top l = l.\\toFinset.\\inf id $$$

Lean4

theorem _root_.List.foldr_inf_eq_inf_toFinset [DecidableEq α] (l : List α) : l.foldr (· ⊓ ·) ⊤ = l.toFinset.inf id :=
  by
  rw [← coe_fold_r, ← Multiset.fold_dedup_idem, inf_def, ← List.toFinset_coe, toFinset_val, Multiset.map_id]
  rfl

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