universallyClosed_isStableUnderBaseChange

English

If f is universally closed, then its base map f.base is a closed map.

Русский

Если f универсально замкнут, то базовая карта f.base является замкнутым отображением.

LaTeX

$$$\\text{IsClosedMap}(f_{\\mathrm{base}})$$$

Lean4

instance universallyClosed_isStableUnderBaseChange : IsStableUnderBaseChange @UniversallyClosed :=
  universallyClosed_eq.symm ▸ universally_isStableUnderBaseChange (topologically @IsClosedMap)

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