Documentation Verification Report

Compactum

📁 Source: Mathlib/Topology/Category/Compactum.lean

Statistics

Metric	Count
Definitions `forgetCreatesLimits`, `Compactum`, `adj`, `forget`, `free`, `homOfContinuous`, `incl`, `instCoeSortType`, `instConcreteCategoryHomA`, `instCreatesLimitsForget`, `instFunLikeHomA`, `instTopologicalSpaceA`, `join`, `ofTopologicalSpace`, `str`, `forgetCreatesLimits`, `compactumToCompHaus`, `isoOfTopologicalSpace`, `compactumToCompHausCompForget`, `instCategoryCompactum`, `instInhabitedCompactum`	21
Theorems `cl_eq_closure`, `continuous_of_hom`, `instCompactSpaceA`, `instFaithfulForget`, `instHasLimits`, `instT2SpaceA`, `isClosed_cl`, `isClosed_iff`, `join_distrib`, `le_nhds_of_str_eq`, `lim_eq_str`, `str_eq_of_le_nhds`, `str_hom_commute`, `str_incl`, `essSurj`, `faithful`, `full`, `isEquivalence`	18
Total	39

CompHaus

Definitions

Name	Category	Theorems
`forgetCreatesLimits` 📖	CompOp	—

Compactum

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`forget` 📖	CompOp	1 math math: `instFaithfulForget`
`free` 📖	CompOp	—
`homOfContinuous` 📖	CompOp	—
`incl` 📖	CompOp	1 math math: `str_incl`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryHomA` 📖	CompOp	2 math math: `continuous_of_hom`, `str_hom_commute`
`instCreatesLimitsForget` 📖	CompOp	—
`instFunLikeHomA` 📖	CompOp	2 math math: `continuous_of_hom`, `str_hom_commute`
`instTopologicalSpaceA` 📖	CompOp	8 math math: `instT2SpaceA`, `cl_eq_closure`, `instCompactSpaceA`, `le_nhds_of_str_eq`, `lim_eq_str`, `continuous_of_hom`, `isClosed_iff`, `isClosed_cl`
`join` 📖	CompOp	1 math math: `join_distrib`
`ofTopologicalSpace` 📖	CompOp	—
`str` 📖	CompOp	6 math math: `lim_eq_str`, `str_incl`, `str_hom_commute`, `str_eq_of_le_nhds`, `isClosed_iff`, `join_distrib`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cl_eq_closure` 📖	mathematical	—	`closure` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instTopologicalSpaceA`	—	`Ultrafilter.lawfulMonad` `Set.ext` `mem_closure_iff_ultrafilter` `le_nhds_of_str_eq` `str_eq_of_le_nhds`
`continuous_of_hom` 📖	mathematical	—	`Continuous` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instTopologicalSpaceA` `DFunLike.coe` `instFunLikeHomA` `CategoryTheory.ConcreteCategory.hom` `Compactum` `instCategoryCompactum` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instConcreteCategoryHomA`	—	`Ultrafilter.lawfulMonad` `continuous_iff_ultrafilter` `Filter.Tendsto.eq_1` `Ultrafilter.coe_map` `le_nhds_of_str_eq` `str_hom_commute` `str_eq_of_le_nhds`
`instCompactSpaceA` 📖	mathematical	—	`CompactSpace` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instTopologicalSpaceA`	—	`Ultrafilter.lawfulMonad` `isCompact_iff_ultrafilter_le_nhds` `le_nhds_iff`
`instFaithfulForget` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Compactum` `instCategoryCompactum` `CategoryTheory.types` `forget`	—	`Ultrafilter.lawfulMonad` `CategoryTheory.Monad.forget_faithful`
`instHasLimits` 📖	mathematical	—	`CategoryTheory.Limits.HasLimits` `Compactum` `instCategoryCompactum`	—	`CategoryTheory.hasLimits_of_hasLimits_createsLimits` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self`
`instT2SpaceA` 📖	mathematical	—	`T2Space` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instTopologicalSpaceA`	—	`Ultrafilter.lawfulMonad` `t2_iff_ultrafilter` `str_eq_of_le_nhds`
`isClosed_cl` 📖	mathematical	—	`IsClosed` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instTopologicalSpaceA`	—	`Ultrafilter.lawfulMonad` `isClosed_iff`
`isClosed_iff` 📖	mathematical	—	`IsClosed` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instTopologicalSpaceA` `Set` `Set.instMembership` `str`	—	`Ultrafilter.lawfulMonad` `isOpen_compl_iff` `Ultrafilter.compl_mem_iff_notMem` `Ultrafilter.mem_or_compl_mem`
`join_distrib` 📖	mathematical	—	`str` `join` `Ultrafilter.map` `Ultrafilter` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter.monad` `Ultrafilter.lawfulMonad`	—	`Ultrafilter.lawfulMonad` `CategoryTheory.Monad.Algebra.assoc`
`le_nhds_of_str_eq` 📖	mathematical	`str`	`Filter` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds` `instTopologicalSpaceA`	—	`Ultrafilter.lawfulMonad` `le_nhds_iff`
`lim_eq_str` 📖	mathematical	—	`Ultrafilter.lim` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instTopologicalSpaceA` `str`	—	`Ultrafilter.lawfulMonad` `Ultrafilter.lim_eq_iff_le_nhds` `instT2SpaceA` `instCompactSpaceA` `le_nhds_iff`
`str_eq_of_le_nhds` 📖	mathematical	`Filter` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds` `instTopologicalSpaceA`	`str`	—	`Ultrafilter.lawfulMonad` `Ultrafilter.compl_mem_iff_notMem` `Ultrafilter.mem_coe` `le_nhds_iff` `IsClosed.isOpen_compl` `isClosed_cl` `Filter.mem_of_superset` `Filter.inter_mem` `FiniteInter.finiteInterClosure_insert` `Filter.univ_sets` `Set.ext` `FiniteInter.finiteInter_mem` `FiniteInter.finiteInterClosure_finiteInter` `Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty` `Ultrafilter.coe_le_coe` `join_distrib` `str_incl`
`str_hom_commute` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.types` `CategoryTheory.ofTypeMonad` `Ultrafilter` `Ultrafilter.monad` `Ultrafilter.lawfulMonad` `instFunLikeHomA` `CategoryTheory.ConcreteCategory.hom` `Compactum` `instCategoryCompactum` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instConcreteCategoryHomA` `str` `Ultrafilter.map`	—	`Ultrafilter.lawfulMonad` `CategoryTheory.Monad.Algebra.Hom.h`
`str_incl` 📖	mathematical	—	`str` `incl`	—	`Ultrafilter.lawfulMonad` `CategoryTheory.Monad.Algebra.unit`

Profinite

Definitions

Name	Category	Theorems
`forgetCreatesLimits` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`Compactum` 📖	CompOp	8 math math: `compactumToCompHaus.full`, `compactumToCompHaus.essSurj`, `compactumToCompHaus.isEquivalence`, `compactumToCompHaus.faithful`, `Compactum.instHasLimits`, `Compactum.continuous_of_hom`, `Compactum.str_hom_commute`, `Compactum.instFaithfulForget`
`compactumToCompHaus` 📖	CompOp	4 math math: `compactumToCompHaus.full`, `compactumToCompHaus.essSurj`, `compactumToCompHaus.isEquivalence`, `compactumToCompHaus.faithful`
`compactumToCompHausCompForget` 📖	CompOp	—
`instCategoryCompactum` 📖	CompOp	8 math math: `compactumToCompHaus.full`, `compactumToCompHaus.essSurj`, `compactumToCompHaus.isEquivalence`, `compactumToCompHaus.faithful`, `Compactum.instHasLimits`, `Compactum.continuous_of_hom`, `Compactum.str_hom_commute`, `Compactum.instFaithfulForget`
`instInhabitedCompactum` 📖	CompOp	—

compactumToCompHaus

Definitions

Name	Category	Theorems
`isoOfTopologicalSpace` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essSurj` 📖	mathematical	—	`CategoryTheory.Functor.EssSurj` `Compactum` `CompHaus` `instCategoryCompactum` `CompHausLike.category` `compactumToCompHaus`	—	`CompHaus.instCompactSpaceCarrierToTopTrue` `CompHaus.instT2SpaceCarrierToTopTrue`
`faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Compactum` `instCategoryCompactum` `CompHaus` `CompHausLike.category` `compactumToCompHaus`	—	`CategoryTheory.Monad.Algebra.Hom.ext` `Ultrafilter.lawfulMonad`
`full` 📖	mathematical	—	`CategoryTheory.Functor.Full` `Compactum` `instCategoryCompactum` `CompHaus` `CompHausLike.category` `compactumToCompHaus`	—	`ContinuousMap.continuous_toFun`
`isEquivalence` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `Compactum` `instCategoryCompactum` `CompHaus` `CompHausLike.category` `compactumToCompHaus`	—	`faithful` `full` `essSurj`

---

← Back to Index