comp — Mathlib

English

The composition of two local homeomorphisms is a local homeomorphism.

Русский

Состав двух локальных гомеоморфизмов является локальной гомеоморфией.

LaTeX

$$$\\operatorname{IsLocalHomeomorph}(g) \\land \\operatorname{IsLocalHomeomorph}(f) \\Rightarrow \\operatorname{IsLocalHomeomorph}(g\\circ f)$$$

Lean4

/-- The composition of local homeomorphisms is a local homeomorphism. -/
protected theorem comp (hg : IsLocalHomeomorph g) (hf : IsLocalHomeomorph f) : IsLocalHomeomorph (g ∘ f) :=
  isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr
    (hg.isLocalHomeomorphOn.comp hf.isLocalHomeomorphOn (Set.univ.mapsTo_univ f))

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