finite_preimage_singleton — Mathlib

English

For a finite morphism f: X → Y and a point y ∈ Y, the preimage of {y} under the base map is finite.

Русский

Для конечного морфизма f: X → Y и точки y ∈ Y, прообраз {y} под базовой картой конечен.

LaTeX

$$$\forall f:X\to Y\;[\operatorname{IsFinite}(f)],\ \forall y\in Y:\; |(f.base)^{-1}({y})|<\infty.$$$

Lean4

theorem finite_preimage_singleton (f : X ⟶ Y) [IsFinite f] (y : Y) : (f.base ⁻¹' { y }).Finite :=
  f.range_fiberι y ▸ Set.finite_range (f.fiberι y).base

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