comp — Mathlib

English

If g and f are local homeomorphs on their respective domains and f maps s into t, then g∘f is a local homeomorph on s.

Русский

Если g и f — локальные гомеоморфы, и f отправляет s в t, то g∘f — локальный гомеоморфизм на s.

LaTeX

$$$IsLocalHomeomorphOn\\, g\\, t \\; \\to\\; IsLocalHomeomorphOn\\, f\\, s \\; \\to\\; Set MapsTo f s t \\to IsLocalHomeomorphOn\\, (g\\circ f)\\, s$$$

Lean4

protected theorem comp (hg : IsLocalHomeomorphOn g t) (hf : IsLocalHomeomorphOn f s) (h : Set.MapsTo f s t) :
    IsLocalHomeomorphOn (g ∘ f) s := by
  intro x hx
  obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)
  obtain ⟨ef, hxf, rfl⟩ := hf x hx
  exact ⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩

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