card_preimage — Mathlib

English

The cardinality of the preimage equals the cardinality of the elements of s that lie in the range of f.

Русский

Число элементов предобраза равно числу элементов s, которые лежат в образе f.

LaTeX

$$$$ |\\mathrm{preimage}(s,f,hf)| = \\big|\\{x \\in s : x \\in \\mathrm{range}(f)\\}\\big|. $$$$

Lean4

theorem card_preimage (s : Finset β) (f : α → β) (hf) [DecidablePred (· ∈ Set.range f)] :
    (s.preimage f hf).card = {x ∈ s | x ∈ Set.range f}.card :=
  card_nbij f (by simp [Set.MapsTo]) (by simpa) (fun b hb ↦ by aesop)

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