card_preimage_of_injOn — Mathlib

English

Let f : α → β and S ⊆ β satisfy that f is injective on f⁻¹(S) and S ⊆ range f. Then card(f⁻¹(S)) = card(S).

Русский

Пусть f : α → β и S ⊆ β удовлетворяют, что на f⁻¹(S) инъективно отображение f, и S ⊆ range f. Тогда card(f⁻¹(S)) = card(S).

LaTeX

$$$$ (f^{-1}(S)).InjOn\ f \wedge S \subseteq \operatorname{range}(f) \implies |f^{-1}(S)| = |S| $$$$

Lean4

theorem card_preimage_of_injOn {f : α → β} {s : Set β} (hf : (f ⁻¹' s).InjOn f) (hsf : s ⊆ range f) :
    Nat.card (f ⁻¹' s) = Nat.card s := by rw [← Nat.card_image_of_injOn hf, image_preimage_eq_iff.2 hsf]

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