Theorems · Theorem · category theory

Stonean.effectiveEpiFamily_tfae

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

Defined in

Mathlib.Topology.Category.Stonean.EffectiveEpi

Cited by

1 results in Mathlib

Foundations

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

Assumes

Finite