effectiveEpi_tfae — Mathlib

English

For Stonean spaces B and X and a morphism π:X⟶B, the three properties EffectiveEpi π, Epi π, and surjectivity of π are mutually equivalent.

Русский

Для каменеподобных пространств B и X и морфизма π: X → B, три свойства: EffectiveEpi π, Epi π и сюръективность π эквивалентны.

LaTeX

$$$\text{TFAE}([\text{EffectiveEpi }\pi, \text{Epi }\pi, \text{Function.Surjective }\pi])$$$

Lean4

theorem effectiveEpi_tfae {B X : Stonean.{u}} (π : X ⟶ B) : TFAE [EffectiveEpi π, Epi π, Function.Surjective π] :=
  by
  tfae_have 1 → 2 := fun _ ↦ inferInstance
  tfae_have 2 ↔ 3 := epi_iff_surjective π
  tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩
  tfae_finish

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