map_comp — Mathlib

English

The map with a composition of two maps equals successive maps.

Русский

Отображение композиции функций равно последовательному отображению.

LaTeX

$$map_comp (f) (g) hf hg hf' hg' K = (K.map g hg hg').map f hf hf'$$

Lean4

theorem map_comp (f : β → γ) (g : α → β) (hf : Continuous f) (hg : Continuous g) (hf' : IsOpenMap f) (hg' : IsOpenMap g)
    (K : CompactOpens α) : K.map (f ∘ g) (hf.comp hg) (hf'.comp hg') = (K.map g hg hg').map f hf hf' :=
  CompactOpens.ext <| Set.image_comp _ _ _

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