ncard_preimage_of_injective_subset_range

English

If f is injective and s is contained in the range of f, then the preimage has the same cardinality as s.

Русский

Если f инъективна и S ⊆ range f, то предобраз имеет ту же кардинал, что и S.

LaTeX

$$$ (f ^{{-1}}' s).ncard = s.ncard $$$

Lean4

theorem ncard_preimage_of_injective_subset_range {s : Set β} (H : f.Injective) (hs : s ⊆ Set.range f) :
    (f ⁻¹' s).ncard = s.ncard := by rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]

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