universallyInjective_eq — Mathlib

English

UniversallyInjective is the universal closure of the property that the underlying map of points is topologically injective.

Русский

UniversallyInjective эквивалентно универсальному замыканию свойства того, что отображение точек подлежащей топологической инъективности.

LaTeX

$$$@\operatorname{UniversallyInjective} = universally (topologically (Injective \cdot)).$$$

Lean4

theorem universallyInjective_eq : @UniversallyInjective = universally (topologically (Injective ·)) := by ext X Y f;
  rw [universallyInjective_iff]

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