Documentation Verification Report

Cover

📁 Source: Mathlib/Topology/MetricSpace/Cover.lean

Statistics

Metric	Count
Definitions `Cover`, `Cover`, `IsCover`	3
Theorems `isCover_image_iff`, `anti`, `closure`, `empty`, `image_lipschitz`, `image_lipschitz_of_surjective`, `isCompact`, `isCompact_closure`, `mono`, `mono_radius`, `nonempty`, `of_maximal_isSeparated`, `of_subset_cthickening`, `of_subset_cthickening_of_lt`, `of_subset_iUnion_closedBall`, `refl`, `rfl`, `singleton_of_ediam_le`, `subset_cthickening`, `subset_iUnion_closedBall`, `exists_finite_isCover_of_isCompact`, `exists_finite_isCover_of_isCompact_closure`, `exists_finite_isCover_of_totallyBounded`, `isCompact_closure_iff_exists_finite_isCover`, `isCover_closure`, `isCover_empty_right`, `isCover_iff_subset_cthickening`, `isCover_iff_subset_iUnion_closedBall`, `isCover_iff_subset_iUnion_closedEBall`, `isCover_iff_subset_iUnion_emetricClosedBall`, `isCover_zero`	31
Total	34

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`Cover` 📖	CompOp	10 math math: `mem_propQCPrecoverage_iff_exists_quasiCompactCover`, `mem_grothendieckTopology_iff`, `AlgebraicGeometry.QuasiCompactCover.exists_hom`, `exists_cover_of_mem_pretopology`, `Cover.sigmaFunctor_obj`, `mem_overGrothendieckTopology`, `Cover.sigmaFunctor_map`, `exists_cover_of_mem_grothendieckTopology`, `mem_smallGrothendieckTopology`, `mem_pretopology_iff`

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`Cover` 📖	CompOp	58 math math: `coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt`, `liftToDiagramLimitObjAux_fac`, `diagram_obj`, `liftToDiagramLimitObjAux_fac_assoc`, `Opens.mayerVietorisSquare_X₃`, `ι_plusCompIso_hom_assoc`, `CondensedMod.isDiscrete_tfae`, `CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf`, `preservesLimitsOfShape_diagramFunctor`, `diagramCompIso_hom_ι`, `CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete`, `CategoryTheory.Meq.pullback_refine`, `TopCat.Sheaf.exact_iff_stalkFunctor_map_exact`, `diagramCompIso_hom_ι_assoc`, `Plus.toPlus_eq_mk`, `Plus.res_mk_eq_mk_pullback`, `CategoryTheory.Presheaf.isLocallySurjective_toSheafify`, `CondensedMod.isDiscrete_iff_isDiscrete_forget`, `CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete`, `CategoryTheory.Presheaf.isLocallyInjective_toSheafify`, `Plus.eq_mk_iff_exists`, `Opens.mayerVietorisSquare_X₂`, `Opens.coe_mayerVietorisSquare_X₁`, `TopCat.Sheaf.IsFlasque.epi_of_shortExact`, `TopCat.Sheaf.sections_exact_of_left_exact`, `diagram_map`, `diagramPullback_app`, `CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf`, `CondensedSet.isDiscrete_tfae`, `CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor`, `CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete`, `diagramFunctor_map`, `TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂`, `diagramFunctor_obj`, `CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete`, `CategoryTheory.Presheaf.isLocallySurjective_toPlus`, `diagramNatTrans_app`, `preservesLimits_diagramFunctor`, `coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app`, `CategoryTheory.Meq.refine_apply`, `Opens.mayerVietorisSquare'_toSquare`, `Opens.coe_mayerVietorisSquare_X₄`, `CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf`, `ι_plusCompIso_hom`, `diagramNatTrans_id`, `AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde`, `AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb`, `CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat`, `diagramNatTrans_zero`, `preservesLimit_diagramFunctor`, `CategoryTheory.Presheaf.isLocallyInjective_toPlus`, `CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf`, `pullback_obj`, `diagramNatTrans_comp`, `Plus.exists_rep`, `Condensed.instAB4CondensedMod`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `CategoryTheory.Meq.pullback_apply`

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCover_image_iff` 📖	mathematical	`Isometry`	`Metric.IsCover` `Set.image`	—	`Set.mem_image_of_mem` `edist_eq` `one_mul` `Metric.IsCover.image_lipschitz` `lipschitz`

Metric

Definitions

Name	Category	Theorems
`IsCover` 📖	MathDef	30 math math: `IsCover.of_subset_cthickening_of_lt`, `IsCover.rfl`, `Delone.DeloneSet.isCover_coveringRadius`, `IsCover.refl`, `isCover_iff_subset_cthickening`, `exists_set_encard_eq_coveringNumber`, `Isometry.isCover_image_iff`, `IsCover.of_maximal_isSeparated`, `IsCover.image_lipschitz_of_surjective`, `exists_finite_isCover_of_isCompact`, `isCover_empty_right`, `IsCover.anti`, `isCover_minimalCover`, `isCompact_closure_iff_exists_finite_isCover`, `exists_finite_isCover_of_totallyBounded`, `IsCover.mono_radius`, `IsCover.mono`, `isCover_iff_subset_iUnion_closedEBall`, `exists_finite_isCover_of_isCompact_closure`, `IsCover.singleton_of_ediam_le`, `isCover_iff_subset_iUnion_closedBall`, `isCover_closure`, `isCover_iff_subset_iUnion_emetricClosedBall`, `IsCover.empty`, `isCover_zero`, `IsCover.image_lipschitz`, `IsCover.closure`, `isCover_maximalSeparatedSet`, `IsCover.of_subset_cthickening`, `IsCover.of_subset_iUnion_closedBall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finite_isCover_of_isCompact` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Set` `Set.instHasSubset` `Set.Finite` `IsCover`	—	`exists_finite_isCover_of_totallyBounded` `IsCompact.totallyBounded`
`exists_finite_isCover_of_isCompact_closure` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `closure`	`Set` `Set.instHasSubset` `Set.Finite` `IsCover`	—	`exists_finite_isCover_of_totallyBounded` `TotallyBounded.subset` `subset_closure` `IsCompact.totallyBounded`
`exists_finite_isCover_of_totallyBounded` 📖	mathematical	`TotallyBounded` `PseudoEMetricSpace.toUniformSpace`	`Set` `Set.instHasSubset` `Set.Finite` `IsCover`	—	`EMetric.totallyBounded_iff'` `ENNReal.coe_pos` `lt_of_le_of_ne'` `zero_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `LT.lt.le`
`isCompact_closure_iff_exists_finite_isCover` 📖	mathematical	—	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `closure` `Set` `Set.instHasSubset` `Set.Finite` `IsCover` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	—	`exists_finite_isCover_of_isCompact_closure` `IsCover.isCompact_closure` `Set.Finite.isCompact`
`isCover_closure` 📖	mathematical	—	`IsCover` `PseudoMetricSpace.toPseudoEMetricSpace` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`isCover_iff_subset_cthickening` `IsClosed.closure_subset_iff` `isClosed_cthickening`
`isCover_empty_right` 📖	mathematical	—	`IsCover` `Set` `Set.instEmptyCollection`	—	`SetRel.isCover_empty_right`
`isCover_iff_subset_cthickening` 📖	mathematical	—	`IsCover` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instHasSubset` `cthickening` `NNReal.toReal`	—	`isCover_iff_subset_iUnion_closedBall` `IsClosed.cthickening_eq_biUnion_closedBall` `NNReal.zero_le_coe`
`isCover_iff_subset_iUnion_closedBall` 📖	mathematical	—	`IsCover` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `closedBall` `NNReal.toReal`	—	—
`isCover_iff_subset_iUnion_closedEBall` 📖	mathematical	—	`IsCover` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `closedEBall` `ENNReal.ofNNReal`	—	—
`isCover_iff_subset_iUnion_emetricClosedBall` 📖	mathematical	—	`IsCover` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `closedEBall` `ENNReal.ofNNReal`	—	`isCover_iff_subset_iUnion_closedEBall`
`isCover_zero` 📖	mathematical	—	`IsCover` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `NNReal.instZero` `Set` `Set.instHasSubset`	—	`Set.iUnion_congr_Prop` `closedEBall_zero` `Set.biUnion_of_singleton`

Metric.IsCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	mathematical	`Set` `Set.instHasSubset` `Metric.IsCover`	`Metric.IsCover`	—	`SetRel.IsCover.anti`
`closure` 📖	mathematical	`Metric.IsCover` `PseudoMetricSpace.toPseudoEMetricSpace`	`Metric.IsCover` `PseudoMetricSpace.toPseudoEMetricSpace` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`Metric.isCover_closure`
`empty` 📖	mathematical	—	`Metric.IsCover` `Set` `Set.instEmptyCollection`	—	`SetRel.IsCover.empty`
`image_lipschitz` 📖	mathematical	`Metric.IsCover` `LipschitzWith`	`Metric.IsCover` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `Set.image`	—	`le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`image_lipschitz_of_surjective` 📖	mathematical	`Metric.IsCover` `Set.preimage` `LipschitzWith`	`Metric.IsCover` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `Set.image`	—	`image_lipschitz` `Set.image_preimage_eq`
`isCompact` 📖	mathematical	`Metric.IsCover` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	—	`IsCompact.of_isClosed_subset` `IsCompact.cthickening` `subset_cthickening` `IsCompact.isClosed` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`isCompact_closure` 📖	mathematical	`Metric.IsCover` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `closure`	—	`isCompact` `closure` `IsCompact.isClosed` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `isClosed_closure`
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `Metric.IsCover`	`Metric.IsCover`	—	`SetRel.IsCover.mono`
`mono_radius` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `Metric.IsCover`	`Metric.IsCover`	—	`SetRel.IsCover.mono_entourage` `le_trans`
`nonempty` 📖	mathematical	`Metric.IsCover` `Set.Nonempty`	`Set.Nonempty`	—	`SetRel.IsCover.nonempty`
`of_maximal_isSeparated` 📖	mathematical	`Maximal` `Set` `Set.instLE` `Set.instHasSubset` `Metric.IsSeparated` `ENNReal.ofNNReal`	`Metric.IsCover`	—	`SetRel.IsCover.of_maximal_isSeparated`
`of_subset_cthickening` 📖	mathematical	`Set` `Set.instHasSubset` `Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal.toReal`	`Metric.IsCover` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`Metric.isCover_iff_subset_cthickening`
`of_subset_cthickening_of_lt` 📖	mathematical	`Set` `Set.instHasSubset` `Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal.toReal` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `NNReal.instPartialOrder`	`Metric.IsCover` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`of_subset_iUnion_closedBall` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Metric.cthickening_subset_iUnion_closedBall_of_lt` `LE.le.trans_lt` `NNReal.zero_le_coe`
`of_subset_iUnion_closedBall` 📖	mathematical	`Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `Metric.closedBall` `NNReal.toReal`	`Metric.IsCover` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`Metric.isCover_iff_subset_iUnion_closedBall`
`refl` 📖	mathematical	—	`Metric.IsCover`	—	`SetRel.IsCover.rfl`
`rfl` 📖	mathematical	—	`Metric.IsCover`	—	`refl`
`singleton_of_ediam_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `ENNReal.ofNNReal` `Set` `Set.instMembership`	`Metric.IsCover` `Set` `Set.instSingletonSet`	—	`LE.le.trans` `Metric.edist_le_ediam_of_mem`
`subset_cthickening` 📖	mathematical	`Metric.IsCover` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set` `Set.instHasSubset` `Metric.cthickening` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal.toReal`	—	`Metric.isCover_iff_subset_cthickening`
`subset_iUnion_closedBall` 📖	mathematical	`Metric.IsCover` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `Metric.closedBall` `NNReal.toReal`	—	`Metric.isCover_iff_subset_iUnion_closedBall`

---

← Back to Index