comp — Mathlib

English

The composition of two ContinuousOpenMaps is itself a ContinuousOpenMap.

Русский

Пусть есть два непрерывных открытых отображения; их композиция снова является непрерывным открытым отображением.

LaTeX

$$$\text{comp} : (f : β \toCO γ) (g : α \toCO β) : α \toCO γ.$$$

Lean4

/-- Composition of `ContinuousOpenMap`s as a `ContinuousOpenMap`. -/
def comp (f : β →CO γ) (g : α →CO β) : ContinuousOpenMap α γ :=
  ⟨f.toContinuousMap.comp g.toContinuousMap, f.map_open'.comp g.map_open'⟩

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