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