effectiveEpiFamily_of_jointly_surjective

English

If for every b in B there exists some a and x with π(a)(x)=b, then the family is effectively epi.

Русский

Если для каждого b в B существует a и x с π(a)(x)=b, то семейство эпиморфно по совокупности.

LaTeX

$$$\\forall b:\\,B,\\exists a:\\,α,\\exists x:\\,X(a),\\ π(a)(x)=b \\Rightarrow \\mathrm{EffectiveEpiFamily} X π$$$

Lean4

theorem effectiveEpiFamily_of_jointly_surjective {α : Type} [Finite α] {B : Profinite.{u}} (X : α → Profinite.{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

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