map_comp — Mathlib

English

Let f: β → γ and g: α → β be continuous with f and g being open maps, and K ∈ PositiveCompacts α. Then the image of K under the composition f ∘ g equals the image under f of the image under g.

Русский

Пусть f: β → γ и g: α → β непрерывны и являются открытыми отображениями, и K ∈ PositiveCompacts α. Тогда образ K при композиции f ∘ g равен образу образа K под g далее под f.

LaTeX

$$$\mathrm{Im}_{f\circ g}(K) = \mathrm{Im}_f(\mathrm{Im}_g(K))$$$

Lean4

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

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