count_injective_image — Mathlib

English

If f is injective and α, β have measurable singleton structures, then count of the image equals count of the domain for any set s.

Русский

Если f инъективна и существуют измеримые одиночки в α и β, то счёт образа равен счёту множества.

LaTeX

$$$\forall s,\; count(f''s) = count(s)$$$

Lean4

theorem count_injective_image [MeasurableSingletonClass α] [MeasurableSingletonClass β] {f : β → α}
    (hf : Function.Injective f) (s : Set β) : count (f '' s) = count s :=
  by
  by_cases hs : s.Finite
  · exact count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet
  rw [count_apply_infinite hs]
  rw [← finite_image_iff hf.injOn] at hs
  rw [count_apply_infinite hs]

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