discrete_fiber — Mathlib

English

If f: X → Y is finite, then for every y ∈ Y the topological space underlying the fiber X_y is discrete.

Русский

Если f: X → Y конечен, то фибра X_y над любой точкой y образует дискретное пространство.

LaTeX

$$$\forall f:X\to Y\;[\operatorname{IsFinite}(f)],\ \forall y\in Y:\; \text{DiscreteTopology}((f.fiber y).\operatorname{carrier}).$$$

Lean4

instance discrete_fiber (f : X ⟶ Y) (y : Y) [IsFinite f] : DiscreteTopology (f.fiber y) :=
  inferInstance

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