Theorems · Definition · category theory

CompHausLike.HasExplicitFiniteCoproduct

{P : TopCat → Prop} → {α : Type w} → (α → CompHausLike P) → Prop

A typeclass describing the property that forming the disjoint union is stable under the property P.

Defined in

Mathlib.Topology.Category.CompHausLike.Limits

Cited by

8 results in Mathlib

Foundations

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