finite_preimage — Mathlib

English

Let f: X → Y be finite and s ⊆ Y finite. Then the preimage f^{-1}(s) is finite.

Русский

Пусть f: X → Y конечен и s ⊆ Y конечно. Тогда прообраз f^{-1}(s) конечен.

LaTeX

$$$\forall f:X\to Y\;[\operatorname{IsFinite}(f)],\ \forall s\subseteq Y:\; s\text{ finite} \Rightarrow (f.base)^{-1}(s)\text{ finite}.$$$

Lean4

theorem finite_preimage (f : X.Hom Y) [IsFinite f] {s : Set Y} (hs : s.Finite) : (f.base ⁻¹' s).Finite :=
  by
  rw [← Set.biUnion_of_singleton s, Set.preimage_iUnion₂]
  exact hs.biUnion fun _ _ ↦ IsFinite.finite_preimage_singleton f _

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