comp

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#IsOpenMap.comp

English

If g and f are open maps, then their composition g ∘ f is an open map.

Русский

Если отображения g и f — открытые, то композиция g ∘ f — открытое отображение.

LaTeX

$$$$IsOpenMap(g) \\rightarrow IsOpenMap(f) \\rightarrow IsOpenMap(g \\circ f)$$$$

Lean4

protected theorem comp (hg : IsOpenMap g) (hf : IsOpenMap f) : IsOpenMap (g ∘ f) := fun s hs => by rw [image_comp];
  exact hg _ (hf _ hs)

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

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

Разделы

Аффилиация

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