Theorems · Definition · category theory
Stonean.compHaus
Stonean → CompHaus
The underlying CompHaus of a Stonean.
- Defined in
- Mathlib.Topology.Category.Stonean.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objproof · cited by 19,642
- CompHausstatement · cited by 61
- Stoneanstatement and proof · cited by 19
- Stonean.toCompHausproof · cited by 5
Cited by7
Results whose statement or proof uses this declaration.
- CompHaus.liftstatement and proof · cited by 3
- Condensed.epi_iff_surjective_on_stoneanstatement and proof · cited by 2
- CompHaus.lift_liftsstatement and proof · cited by 1
- CompHaus.lift.congr_simpstatement and proof · cited by 0
- CondensedMod.epi_iff_surjective_on_stoneanstatement · cited by 0
- CompHaus.lift_lifts_assocstatement and proof · cited by 0
- CondensedSet.epi_iff_surjective_on_stoneanstatement · cited by 0