eq — Mathlib · SciLib

English

UniversallyOpen is the universal closure of the property that the underlying topological map is an open map.

Русский

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

LaTeX

$$$@\operatorname{UniversallyOpen} = universally (topologically @IsOpenMap).$$$

Lean4

theorem eq : @UniversallyOpen = universally (topologically @IsOpenMap) := by ext X Y f; rw [universallyOpen_iff]

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