comap_injective — Mathlib

English

A protected version of the composition property for comap with continuous maps.

Русский

Защищенная версия свойства композиции для обратного образа при непрерывных отображениях.

LaTeX

$$$\operatorname{comap}(g\circ f) = (\operatorname{comap} f) . (\operatorname{comap} g)$$$

Lean4

theorem comap_injective [T0Space β] : Injective (comap : C(α, β) → FrameHom (Opens β) (Opens α)) := fun f g h =>
  ContinuousMap.ext fun a =>
    Inseparable.eq <|
      inseparable_iff_forall_isOpen.2 fun s hs =>
        have : comap f ⟨s, hs⟩ = comap g ⟨s, hs⟩ := DFunLike.congr_fun h ⟨_, hs⟩
        show a ∈ f ⁻¹' s ↔ a ∈ g ⁻¹' s from Set.ext_iff.1 (coe_inj.2 this) a

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