Documentation Verification Report

Dense

📁 Source: Mathlib/CategoryTheory/Presentable/Dense.lean

Statistics

Metric	Count
Definitions `Dense`	1
Theorems `final_toCostructuredArrow`, `instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι`, `instIsDenseFullSubcategoryIsCardinalPresentableι`, `instEssentiallySmallIsFinitelyPresentable`, `instIsDenseFullSubcategoryIsFinitelyPresentableι`, `instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι`, `isCardinalFilteredGenerator_isCardinalPresentable`	7
Total	8

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCardinalFilteredGenerator_isCardinalPresentable` 📖	mathematical	—	`ObjectProperty.IsCardinalFilteredGenerator` `isCardinalPresentable`	—	`HasCardinalFilteredGenerator.exists_generator` `IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator` `ObjectProperty.IsCardinalFilteredGenerator.of_le_isoClosure` `ObjectProperty.isoClosure_eq_self` `instIsClosedUnderIsomorphismsIsCardinalPresentable` `ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable` `le_rfl`

CategoryTheory.IsCardinalAccessibleCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`final_toCostructuredArrow` 📖	mathematical	—	`CategoryTheory.Functor.Final` `CategoryTheory.CostructuredArrow` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.isCardinalPresentable` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.instCategoryCostructuredArrow` `CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow`	—	`CategoryTheory.isFiltered_of_isCardinalFiltered` `CategoryTheory.Functor.final_iff_of_isFiltered` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit` `CategoryTheory.instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι` `CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit'` `CategoryTheory.instIsCardinalPresentableObjIsCardinalPresentable` `CategoryTheory.CostructuredArrow.w` `CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj` `CategoryTheory.ObjectProperty.hom_ext`
`instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι` 📖	mathematical	—	`CategoryTheory.IsCardinalFiltered` `CategoryTheory.CostructuredArrow` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.isCardinalPresentable` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.instCategoryCostructuredArrow`	—	`CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape` `CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentable` `CategoryTheory.IsCardinalFiltered.of_final` `final_toCostructuredArrow` `CategoryTheory.essentiallySmall_of_small_of_locallySmall` `UnivLE.small` `UnivLE.self` `CategoryTheory.locallySmall_of_univLE`
`instIsDenseFullSubcategoryIsCardinalPresentableι` 📖	mathematical	—	`CategoryTheory.Functor.IsDense` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.isCardinalPresentable` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.ι`	—	`CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape` `CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentable` `final_toCostructuredArrow` `CategoryTheory.essentiallySmall_of_small_of_locallySmall` `UnivLE.small` `UnivLE.self` `CategoryTheory.locallySmall_of_univLE` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`

CategoryTheory.IsFinitelyAccessibleCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEssentiallySmallIsFinitelyPresentable` 📖	mathematical	—	`CategoryTheory.ObjectProperty.EssentiallySmall` `CategoryTheory.ObjectProperty.isFinitelyPresentable`	—	`Cardinal.fact_isRegular_aleph0` `CategoryTheory.ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable` `CategoryTheory.instEssentiallySmallIsCardinalPresentableOfHasCardinalFilteredGenerator` `CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator`
`instIsDenseFullSubcategoryIsFinitelyPresentableι` 📖	mathematical	—	`CategoryTheory.Functor.IsDense` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.isFinitelyPresentable` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.ι`	—	`Cardinal.fact_isRegular_aleph0` `CategoryTheory.ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable` `CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι`
`instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι` 📖	mathematical	—	`CategoryTheory.IsFiltered` `CategoryTheory.CostructuredArrow` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.isFinitelyPresentable` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.instCategoryCostructuredArrow`	—	`Cardinal.fact_isRegular_aleph0` `CategoryTheory.isCardinalFiltered_aleph0_iff` `CategoryTheory.ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable` `CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι`

(root)

Definitions

Name	Category	Theorems
`Dense` 📖	MathDef	98 math math: `ContinuousMap.dense_setOf_contDiff`, `eventually_residual`, `AddAction.isTopologicallyTransitive_iff_dense_iUnion_preimage`, `dense_iff_exists_between`, `MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage`, `ContDiff.dense_compl_range_of_finrank_lt_finrank`, `Subgroup.dense_of_not_isolated_one`, `dense_of_mem_residual`, `Submodule.dense_iff_topologicalClosure_eq_top`, `AlgebraicGeometry.Scheme.RationalMap.dense_domain`, `EMetric.dense_iff`, `AddSubgroup.dense_of_no_min`, `IsOpen.dense_of_preimage_vadd_invariant`, `dense_liouville`, `dense_coborder`, `dense_closure`, `Subtype.dense_iff`, `dense_univ`, `dense_iUnion_interior_of_closed`, `denseRange_subtype_val`, `MeasureTheory.Measure.dense_of_ae`, `IsOpen.dense_of_preimage_smul_invariant`, `IsOpenQuotientMap.dense_preimage_iff`, `dense_discrete`, `AddCircle.dense_addSubgroup_iff_ne_zmultiples`, `Metric.dense_iff_iUnion_ball`, `MeasureTheory.dense_of_generateFrom_isSetRing`, `Metric.dense_iUnion_range_toInductiveLimit`, `UniqueDiffWithinAt.dense_tangentConeAt`, `dense_biUnion_interior_of_closed`, `ContDiffOn.dense_compl_image_of_dimH_lt_finrank`, `MeasureTheory.dense_of_generateFrom_isSetSemiring`, `dense_sUnion_interior_of_closed`, `dense_irrational`, `dense_iff_closure_eq`, `IsOpen.dense_iUnion_preimage_vadd`, `uniqueDiffWithinAt_iff`, `AddSubgroup.dense_iff_ne_zmultiples`, `isClosed_isNowhereDense_iff_compl`, `dense_of_nonempty_vadd_invariant`, `MeasureTheory.Lp.boundedContinuousFunction_dense`, `dense_differentiableAt_norm`, `IsOpen.dense_iUnion_preimage_smul`, `dense_addSubmonoidClosure_iff_addSubgroupClosure`, `QuotientGroup.dense_preimage_mk`, `IsSelfAdjoint.dense_domain`, `MulAction.dense_orbit`, `IsDenseEmbedding.dense_image`, `Metric.dense_iff`, `Subgroup.dense_or_cyclic`, `Set.Countable.dense_compl`, `dense_compl_singleton_iff_not_open`, `IsOpen.dense_iUnion_smul`, `IsOpen.dense`, `AddAction.IsMinimal.dense_orbit`, `TopologicalSpace.exists_countable_dense`, `QuotientAddGroup.dense_image_mk`, `mem_residual`, `Rat.dense_compl_compact`, `dense_submonoidClosure_iff_subgroupClosure`, `AddAction.dense_orbit`, `QuotientAddGroup.dense_preimage_mk`, `dense_addSubgroupClosure_pair_iff`, `AddAction.isTopologicallyTransitive_iff_dense_iUnion`, `dense_of_nonempty_smul_invariant`, `IsDenseInducing.dense_image`, `dense_compl_singleton`, `dense_iff_inter_open`, `LinearMap.isClosed_or_dense_ker`, `MulAction.isTopologicallyTransitive_iff_dense_iUnion`, `AddSubgroup.dense_or_cyclic`, `AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField`, `MulAction.IsMinimal.dense_orbit`, `Topology.IsInducing.dense_iff`, `AddAction.isTopologicallyTransitive_iff_dense_of_preimage_invariant`, `Subgroup.dense_of_no_min`, `AlgebraicGeometry.Scheme.PartialMap.dense_domain`, `dense_compl_of_dimH_lt_finrank`, `exists_countable_dense_bot_top`, `ContinuousMapZero.adjoin_id_dense`, `MeasureTheory.Lp.dense_hasCompactSupport_contDiff`, `AddSubgroup.dense_of_not_isolated_zero`, `interior_eq_empty_iff_dense_compl`, `TopologicalSpace.separableSpace_iff`, `exists_countable_dense_no_bot_top`, `QuotientGroup.dense_image_mk`, `MulAction.isTopologicallyTransitive_iff_dense_of_preimage_invariant`, `Subgroup.dense_xor'_cyclic`, `mem_residual_iff`, `TopologicalSpace.SeparableSpace.exists_countable_dense`, `IsOpen.dense_iUnion_vadd`, `dense_of_exists_between`, `TopologicalSpace.IsTopologicalBasis.dense_iff`, `MeasureTheory.Lp.simpleFunc.dense`, `ENNReal.exists_countable_dense_no_zero_top`, `Submodule.isClosed_or_dense_of_isCoatom`, `AddSubgroup.dense_xor'_cyclic`, `Subgroup.dense_iff_ne_zpowers`

---

← Back to Index