comap_comap — Mathlib

English

Composing preimages commutes: (K.comap f₂ hf₂).comap f₁ hf₁ = K.comap (f₂ ∘ f₁) (hf₂ ∘ hf₁).

Русский

Сочетание предобразований соответствует композиции функций: (K.comap f₂ hf₂).comap f₁ hf₁ = K.comap (f₂ ∘ f₁) (hf₂ ∘ hf₁).

LaTeX

$$$$ (K^{\\mathrm{comap} f_2 hf_2})^{\\mathrm{comap} f_1 hf_1} = K^{\\mathrm{comap} (f_2 \\circ f_1) (hf_2 \\circ hf_1)}. $$$$

Lean4

@[to_additive]
theorem comap_comap {P : Type*} [Group P] [TopologicalSpace P] (K : OpenSubgroup P) (f₂ : N →* P) (hf₂ : Continuous f₂)
    (f₁ : G →* N) (hf₁ : Continuous f₁) : (K.comap f₂ hf₂).comap f₁ hf₁ = K.comap (f₂.comp f₁) (hf₂.comp hf₁) :=
  rfl

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