Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `CompHaus`, `instCoeSortType`, `instInhabited`, `limitCone`, `limitConeIsLimit`, `of`, `compHausLikeToCompHaus`, `compHausToTop`, `createsLimits`, `reflective`, `stoneCechEquivalence`, `stoneCechObj`, `topToCompHaus`	13
Theorems `epi_iff_surjective`, `hasColimits`, `hasLimits`, `instCompactSpaceCarrierToTopTrue`, `instHasPropTrue`, `instT2SpaceCarrierToTopTrue`, `stoneCechObj_toTop_carrier`, `topToCompHaus_obj`	8
Total	21

CompHaus

Definitions

Name	Category	Theorems
`instCoeSortType` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`limitCone` 📖	CompOp	1 math math: `LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus`
`limitConeIsLimit` 📖	CompOp	—
`of` 📖	CompOp	8 math math: `condensedSetToTopCat_obj_carrier`, `CondensedSet.topCatAdjunctionUnit_val_app_apply`, `CondensedSet.continuous_coinducingCoprod`, `CondensedSet.topCatAdjunctionUnit_val_app`, `projective_ultrafilter`, `Condensed.underlying_obj`, `CondensedSet.toTopCatMap_hom_apply`, `Condensed.underlying_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_surjective` 📖	mathematical	—	`CategoryTheory.Epi` `CompHaus` `CompHausLike.category` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `IsCompact.isClosed` `instT2SpaceCarrierToTopTrue` `isCompact_range` `instCompactSpaceCarrierToTopTrue` `ContinuousMap.continuous` `isClosed_singleton` `T2Space.t1Space` `Set.disjoint_singleton_right` `exists_continuous_zero_one_of_isClosed` `NormalSpace.of_regularSpace_lindelofSpace` `instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space` `instWeaklyLocallyCompactSpaceOfCompactSpace` `T2Space.r1Space` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `Homeomorph.compactSpace` `compactSpace_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `Homeomorph.t2Space` `instT2SpaceSubtype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompHausLike.is_compact` `CompHausLike.is_hausdorff` `instHasPropTrue` `Continuous.comp` `continuous_uliftUp` `Set.left_mem_Icc` `zero_le_one` `Real.instZeroLEOneClass` `continuous_const` `CategoryTheory.cancel_epi` `CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext` `ULift.ext` `CategoryTheory.comp_apply` `Set.mem_range_self` `zero_ne_one` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Set.mem_singleton` `CategoryTheory.epi_iff_surjective` `CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `CategoryTheory.instFaithfulForget`
`hasColimits` 📖	mathematical	—	`CategoryTheory.Limits.HasColimits` `CompHaus` `CompHausLike.category`	—	`CategoryTheory.hasColimits_of_reflective` `TopCat.topCat_hasColimits`
`hasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `CompHaus` `CompHausLike.category`	—	`CategoryTheory.hasLimits_of_hasLimits_createsLimits` `TopCat.topCat_hasLimits`
`instCompactSpaceCarrierToTopTrue` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str`	—	`CompHausLike.is_compact`
`instHasPropTrue` 📖	mathematical	—	`CompHausLike.HasProp`	—	—
`instT2SpaceCarrierToTopTrue` 📖	mathematical	—	`T2Space` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str`	—	`CompHausLike.is_hausdorff`

(root)

Definitions

Name	Category	Theorems
`CompHaus` 📖	CompOp	68 math math: `condensedSetToTopCat_obj_carrier`, `Condensed.hom_ext_iff`, `CondensedMod.isDiscrete_tfae`, `CondensedSet.hom_naturality_apply`, `CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf`, `Condensed.discrete_map`, `Stonean.instEffectivelyEnoughCompHausToCompHaus`, `CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete`, `CompHaus.hasColimits`, `compactumToCompHaus.full`, `instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed`, `CompHaus.instEnoughProjectives`, `instFullCompHausCondensedTypeCompHausToCondensed'`, `compactumToCompHaus.essSurj`, `Condensed.instPreservesFiniteProductsOppositeCompHausVal`, `CondensedMod.isDiscrete_iff_isDiscrete_forget`, `compactumToCompHaus.isEquivalence`, `CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete`, `instFullCompHausCondensedSetCompHausToCondensed`, `CompHaus.lift_lifts`, `CondensedMod.epi_iff_surjective_on_stonean`, `CondensedSet.epi_iff_surjective_on_stonean`, `CondensedSet.topCatAdjunctionUnit_val_app_apply`, `compactumToCompHaus.faithful`, `Condensed.comp_val`, `Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus`, `CondensedMod.hom_naturality_apply`, `instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus`, `Condensed.epi_iff_locallySurjective_on_compHaus`, `CompHaus.toProfinite_obj'`, `Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus`, `CondensedSet.continuous_coinducingCoprod`, `CompHausOpToFrame.faithful`, `CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf`, `CondensedSet.topCatAdjunctionUnit_val_app`, `CompHaus.instPreregular`, `CompHaus.lift_lifts_assoc`, `CondensedSet.isDiscrete_tfae`, `LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus`, `CompHaus.effectiveEpi_tfae`, `CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete`, `instFaithfulCompHausCondensedTypeCompHausToCondensed'`, `CompHaus.presentation.epi_π`, `CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete`, `Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus`, `CompHaus.hasLimits`, `CondensedMod.epi_iff_locallySurjective_on_compHaus`, `CompHaus.projective_ultrafilter`, `Stonean.instReflectsEffectiveEpisCompHausToCompHaus`, `CompHaus.epi_iff_surjective`, `instFaithfulCompHausCondensedSetCompHausToCondensed`, `Stonean.instProjectiveCompHausCompHaus`, `CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf`, `CompHaus.Gleason`, `Condensed.underlying_obj`, `CondensedSet.toTopCatMap_hom_apply`, `Condensed.underlying_map`, `CompHaus.effectiveEpiFamily_tfae`, `CondensedSet.epi_iff_locallySurjective_on_compHaus`, `CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf`, `Condensed.id_val`, `Stonean.instPreservesEffectiveEpisCompHausToCompHaus`, `Condensed.instAB4CondensedMod`, `Condensed.equalizerCondition`, `Condensed.discrete_obj`, `CompHausToLocale.faithful`, `topToCompHaus_obj`
`compHausLikeToCompHaus` 📖	CompOp	—
`compHausToTop` 📖	CompOp	2 math math: `CompHausOpToFrame.faithful`, `CompHausToLocale.faithful`
`stoneCechEquivalence` 📖	CompOp	—
`stoneCechObj` 📖	CompOp	1 math math: `stoneCechObj_toTop_carrier`
`topToCompHaus` 📖	CompOp	1 math math: `topToCompHaus_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stoneCechObj_toTop_carrier` 📖	mathematical	—	`TopCat.carrier` `CompHausLike.toTop` `stoneCechObj` `StoneCech` `TopCat.str`	—	—
`topToCompHaus_obj` 📖	mathematical	—	`TopCat.carrier` `CompHausLike.toTop` `CategoryTheory.Functor.obj` `TopCat` `TopCat.instCategory` `CompHaus` `CompHausLike.category` `topToCompHaus` `StoneCech` `TopCat.str`	—	—

compHausToTop

Definitions

Name	Category	Theorems
`createsLimits` 📖	CompOp	—
`reflective` 📖	CompOp	—

---

← Back to Index