univ_filter_exists — Mathlib

English

The universal filter of a predicate asserting the existence of a preimage equals the universal image: univ.filter (λ y, ∃ x, f x = y) = univ.image f.

Русский

Универсальный фильтр предиката, утверждающего существование прообраза, равен универсума образу: univ.filter (λ y, ∃ x, f x = y) = univ.image f.

LaTeX

$$$\\mathrm{univ.filter}\\ (\\lambda y. \\exists x, f x = y) = \\mathrm{univ.image}\\ f$$$

Lean4

@[simp]
theorem univ_filter_exists (f : α → β) [Fintype β] [DecidablePred fun y => ∃ x, f x = y] [DecidableEq β] :
    (Finset.univ.filter fun y => ∃ x, f x = y) = Finset.univ.image f :=
  by
  ext
  simp

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