map_comp — Mathlib

English

For f : β → γ, g : α → β, and compact K, the map of the composition equals the composition of maps: K.map(f ∘ g) (hf.comp hg) = (K.map g hg).map f hf.

Русский

Для отображений f : β → γ, g : α → β и компактного множества K верно: K.map(f ∘ g) (hf.comp hg) = (K.map g hg).map f hf.

LaTeX

$$$\\forall {f : \\beta \\rightarrow \\gamma} {g : \\alpha \\rightarrow \\beta} (hf : Continuous f) (hg : Continuous g) (K : \\mathrm{Compacts}(\\alpha)),\\\\ K.map (f \\circ g) (hf \\circ hg) = (K.map g hg).map f hf$$$

Lean4

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

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