univ_filter_mem_range — Mathlib

English

For f : α → β, univ.filter (y ∈ Set.range f) = univ.image f.

Русский

Для отображения f : α → β, univ.filter по принадлежности Set.range f равно univ.image f.

LaTeX

$$$ (univ.filter (\\lambda y, y \\in \\mathrm{Set.range}\\ f)) = univ.image f $$$

Lean4

/-- Note this is a special case of `(Finset.image_preimage f univ _).symm`. -/
theorem univ_filter_mem_range (f : α → β) [Fintype β] [DecidablePred fun y => y ∈ Set.range f] [DecidableEq β] :
    (Finset.univ.filter fun y => y ∈ Set.range f) = Finset.univ.image f := by grind

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