isClosedMap_isStableUnderComposition

Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.isClosedMap_isStableUnderComposition

← MathLib Explorer

English

The class of closed maps is stable under composition.

Русский

Класс замкнутых отображений стабилен по композиции.

LaTeX

$$$(\\text{topologically } \\mathrm{IsClosedMap}).IsStableUnderComposition$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru