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