Projective

📁 Source: Mathlib/Topology/Category/CompHaus/Projective.lean

Statistics

Metric	Count
Definitions projectivePresentation	1
Theorems instEnoughProjectives, projective_ultrafilter	2
Total	3

CompHaus

Definitions

Name	Category	Theorems
projectivePresentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEnoughProjectives 📖	mathematical	—	CategoryTheory.EnoughProjectives CompHaus CompHausLike.category	—	—
projective_ultrafilter 📖	mathematical	—	CategoryTheory.Projective CompHaus CompHausLike.category of Ultrafilter Ultrafilter.topologicalSpace ultrafilter_compact Ultrafilter.t2Space	—	ultrafilter_compact Ultrafilter.t2Space Function.Surjective.hasRightInverse epi_iff_surjective continuous_ultrafilter_extend instT2SpaceCarrierToTopTrue instCompactSpaceCarrierToTopTrue instHasPropTrue CompHausLike.is_compact CompHausLike.is_hausdorff CategoryTheory.ConcreteCategory.coe_ext Function.RightInverse.comp_eq_id DenseRange.equalizer denseRange_pure Continuous.comp ContinuousMap.continuous Function.comp_assoc ultrafilter_extend_extends

---

← Back to Index