English
Let α be a finite index set and X : α → CompHaus, with morphisms π_a : X(a) → B to a fixed compact Hausdorff space B. If the family {π_a} is jointly surjective, i.e. every b ∈ B lies in the image of some π_a, then {π_a}_{a∈α} forms an effective epi family.
Русский
Пусть α конечно, X : α → CompHaus и для каждого a ∈ α задан морфизм π_a : X(a) → B в фиксированное компактное и Hausdorff-пространство B. Если семейство морфизмов jointly surjective, то есть каждый элемент b ∈ B лежит в образе некоторого π_a, то семейство π_a образует эффективное эпиморфное семейство.
LaTeX
$$$\left(\forall b \in B,\, \exists a \in \alpha,\, \exists x \in X(a),\, \pi_a(x)=b\right) \Rightarrow \operatorname{EffectiveEpiFamily}(X,\pi)$$$
Lean4
theorem effectiveEpiFamily_of_jointly_surjective {α : Type} [Finite α] {B : CompHaus.{u}} (X : α → CompHaus.{u})
(π : (a : α) → (X a ⟶ B)) (surj : ∀ b : B, ∃ (a : α) (x : X a), π a x = b) : EffectiveEpiFamily X π :=
((effectiveEpiFamily_tfae X π).out 2 0).mp surj
