instIsStableUnderCompositionSchemeTopologicallyIsOpenMap

English

The class (topologically IsOpenMap) is stable under composition, hence UniversallyOpen is closed under composition.

Русский

Класс (topologically IsOpenMap) стабилен при композиции, следовательно UniversallyOpen замкнут относительно композиции.

LaTeX

$$$(topologically \; IsOpenMap).IsStableUnderComposition$$$

Lean4

instance : IsStableUnderComposition (topologically @IsOpenMap) where
  comp_mem f g hf hg := IsOpenMap.comp (f := f.base) (g := g.base) hg hf

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