preimage_of_injOn — Mathlib

English

If s is countable, and InjOn f (f^{-1} s), then the preimage f^{-1}(s) is countable.

Русский

Если s счетно, и InjOn f (f^{-1} s), то предобраз f^{-1}(s) счетен.

LaTeX

$$$\\operatorname{Countable}(s) \\Rightarrow \\exists f:\\ alpha\\to beta, \\operatorname{InjOn}(f, f^{-1}(s)) \\Rightarrow (f^{-1}(s)).Countable$$$

Lean4

theorem preimage_of_injOn {s : Set β} (hs : s.Countable) {f : α → β} (hf : InjOn f (f ⁻¹' s)) : (f ⁻¹' s).Countable :=
  (mapsTo_preimage f s).countable_of_injOn hf hs

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