toFinset_filterMap — Mathlib

English

For any f and inj-condition, (List.filterMap f s).toFinset = s.toFinset.filterMap f f_inj.

Русский

Для списка и условия инъективности: (List.filterMap f s).toFinset = s.toFinset.filterMap f f_inj.

LaTeX

$$$ (List.filterMap f s).toFinset = s.toFinset.filterMap f f_{inj} $$$

Lean4

theorem _root_.List.toFinset_filterMap [DecidableEq α] [DecidableEq β]
    (f_inj : ∀ (a a' : α) (b : β), f a = some b → f a' = some b → a = a') (s : List α) :
    (s.filterMap f).toFinset = s.toFinset.filterMap f f_inj := by simp [← Finset.coe_inj]

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