count_injective_image' — Mathlib

English

If f is injective, then the counting measure of the image f''s equals the counting measure of s, for measurable s and f''s measurable.

Русский

Если f — инъекция, то счётная мера образа f''s равна счётной мере s при измеримом s и измеримом образе.

LaTeX

$$$\text{count}(f''s) = \text{count}(s)$$$

Lean4

theorem count_injective_image' {f : β → α} (hf : Function.Injective f) {s : Set β} (s_mble : MeasurableSet s)
    (fs_mble : MeasurableSet (f '' s)) : count (f '' s) = count s := by
  classical
  by_cases hs : s.Finite
  · lift s to Finset β using hs
    rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble, s.card_image_of_injective hf]
    simpa only [Finset.coe_image] using fs_mble
  · rw [count_apply_infinite hs]
    rw [← finite_image_iff hf.injOn] at hs
    rw [count_apply_infinite hs]

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