English
A map f between topological spaces is specializing if specialization lifts along f; i.e., for every f(x′) ⤳ y there exists x with x′ ⤳ x and f(x) = y.
Русский
Отображение f между топологическими пространствами специализирующее, если специализации поднимаются через f; т.е. для любого f(x′) ⤳ y существует x, такой что x′ ⤳ x и f(x) = y.
LaTeX
$$$\text{SpecializingMap}(f) \iff \forall x', y, f(x') \;\text{Specializes}\; y \Rightarrow \exists x\; (x' \;\text{Specializes}\; x) \land f(x) = y$$$
Lean4
/-- A map `f` between topological spaces is specializing if specializations lifts along `f`,
i.e. for each `f x' ⤳ y` there is some `x` with `x' ⤳ x` whose image is `y`. -/
def SpecializingMap (f : X → Y) : Prop :=
Relation.Fibration (flip (· ⤳ ·)) (flip (· ⤳ ·)) f
