effectiveEpi_iff_surjective — Mathlib

English

In LightProfinite, effective epis are equivalent to surjective maps: EffectiveEpi f iff f is surjective.

Русский

В LightProfinite эффективные эпиморфизмы эквивалентны сюръективным отображениям: EffectiveEpi f ⇔ Surjective f.

LaTeX

$$$\mathrm{EffectiveEpi}(f) \iff \mathrm{Surjective}(f)$$$

Lean4

theorem effectiveEpi_iff_surjective {X Y : LightProfinite.{u}} (f : X ⟶ Y) : EffectiveEpi f ↔ Function.Surjective f :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨effectiveEpiStruct f h⟩⟩⟩
  rw [← epi_iff_surjective]
  infer_instance

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