instPreservesEffectiveEpisCompHausProfiniteToCompHaus

English

The functor profiniteToCompHaus preserves effective epimorphisms, i.e., effective epis in Profinite map to effective epis in CompHaus.

Русский

Функтор profiniteToCompHaus сохраняет эффективные эпиморфизмы: эффективные эпиморфизмы в Profinite переходят в эффективные эпиморфизмы в CompHaus.

LaTeX

$$$\\mathrm{Profinite}.\\mathrm{instPreservesEffectiveEpis}\\;:\\; \\mathrm{Profinite}\\to\\mathrm{CompHaus}\\ \\text{preserves }\\mathrm{EffectiveEpi}$$$

Lean4

instance : profiniteToCompHaus.PreservesEffectiveEpis where
  preserves f h := ((CompHaus.effectiveEpi_tfae _).out 0 2).mpr (((Profinite.effectiveEpi_tfae _).out 0 2).mp h)

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