Theorems · Theorem · category theory

Stonean.effectiveEpiFamily_of_jointly_surjective

∀ {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B),
  (∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b) → CategoryTheory.EffectiveEpiFamily X π

Defined in

Mathlib.Topology.Category.Stonean.EffectiveEpi

Cited by

0 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Finite