Cover

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

Statistics

Metric	Count
Definitions Cover, Cover, IsCover	3
Theorems 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	30
Total	33

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
Cover 📖	CompOp	2 math math: Cover.sigmaFunctor_obj, Cover.sigmaFunctor_map

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
Cover 📖	CompOp	47 math math: coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, liftToDiagramLimitObjAux_fac, diagram_obj, liftToDiagramLimitObjAux_fac_assoc, Opens.mayerVietorisSquare_X₃, CondensedMod.isDiscrete_tfae, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, preservesLimitsOfShape_diagramFunctor, diagramCompIso_hom_ι, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, CategoryTheory.Meq.pullback_refine, diagramCompIso_hom_ι_assoc, CategoryTheory.Presheaf.isLocallySurjective_toSheafify, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, CategoryTheory.Presheaf.isLocallyInjective_toSheafify, Opens.mayerVietorisSquare_X₂, Opens.coe_mayerVietorisSquare_X₁, diagram_map, diagramPullback_app, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, CondensedSet.isDiscrete_tfae, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, diagramFunctor_map, 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, diagramNatTrans_id, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, CategoryTheory.Functor.SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, diagramNatTrans_zero, preservesLimit_diagramFunctor, CategoryTheory.Presheaf.isLocallyInjective_toPlus, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, pullback_obj, diagramNatTrans_comp, Condensed.instAB4CondensedMod, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, CategoryTheory.Meq.pullback_apply

Metric

Definitions

Name	Category	Theorems
IsCover 📖	MathDef	23 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, IsCover.of_maximal_isSeparated, exists_finite_isCover_of_isCompact, isCover_empty_right, isCover_minimalCover, isCompact_closure_iff_exists_finite_isCover, exists_finite_isCover_of_totallyBounded, 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_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 NNReal.instCanonicallyOrderedAdd 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 instZeroNNReal Set Set.instHasSubset	—	Set.iUnion_congr_Prop closedEBall_zero Set.biUnion_of_singleton

Metric.IsCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anti 📖	—	Set Set.instHasSubset Metric.IsCover	—	—	SetRel.IsCover.anti
closure 📖	mathematical	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	NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal 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	NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Set.image	—	image_lipschitz Set.image_preimage_eq
isCompact 📖	—	Metric.IsCover EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace 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	closure	—	isCompact closure IsCompact.isClosed TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace isClosed_closure
mono 📖	—	Set Set.instHasSubset Metric.IsCover	—	—	SetRel.IsCover.mono
mono_radius 📖	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Metric.IsCover	—	—	SetRel.IsCover.mono_entourage le_trans
nonempty 📖	—	Metric.IsCover 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	—	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 instPartialOrderNNReal	Metric.IsCover	—	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.instSingletonSet	—	LE.le.trans Metric.edist_le_ediam_of_mem
subset_cthickening 📖	mathematical	Metric.IsCover PseudoMetricSpace.toPseudoEMetricSpace	Set Set.instHasSubset Metric.cthickening 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