comap — Mathlib

English

Pull back a discrete quotient along a continuous map to obtain a new discrete quotient on the domain.

Русский

Тянем назад факторпространство вдоль непрерывного отображения, получая новое дискретное факторпространство на области определения.

LaTeX

$$$ \\text{comap}(S; f) : \\text{DiscreteQuotient}(X) \\text{ where } R_{X} = \\text{comap}_{f}(R_{Y})$$$

Lean4

/-- Comap a discrete quotient along a continuous map. -/
def comap (S : DiscreteQuotient Y) : DiscreteQuotient X
    where
  toSetoid := Setoid.comap f S.1
  isOpen_setOf_rel _ := (S.2 _).preimage f.continuous

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