Theorems · Theorem · category theory

CompHaus.effectiveEpiFamily_tfae

∀ {α : Type} [inst : Finite α] {B : CompHaus} (X : α → CompHaus) (π : (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.CompHaus.EffectiveEpi

Cited by

3 results in Mathlib

Foundations

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

Assumes

Finite