Documentation Verification Report

UniformConvergence

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

Statistics

Metric	Count
Definitions `instEDist`, `instEMetricSpace`, `instMetricSpaceOfBoundedSpace`, `instPseudoEMetricSpace`, `instPseudoMetricSpaceOfBoundedSpace`, `instEDistOfFiniteElemSet`, `instPseudoEMetricSpace`, `instPseudoMetricSpaceOfBoundedSpace`	8
Theorems `uniformEquicontinuousOn`, `uniformEquicontinuous`, `dist_def`, `dist_le`, `edist_continuousMapMk`, `edist_def`, `edist_eval_le`, `edist_le`, `instBoundedSpace`, `isometry_ofFun_boundedContinuousFunction`, `isometry_ofFun_continuousMap`, `lipschitzOnWith_iff`, `lipschitzOnWith_ofFun_iff`, `lipschitzWith_eval`, `lipschitzWith_iff`, `lipschitzWith_ofFun_iff`, `continuous_of_forall_lipschitzWith`, `edist_continuousRestrict`, `edist_continuousRestrict_of_singleton`, `edist_def`, `edist_def'`, `edist_eq_pi_restrict`, `edist_eq_restrict_sUnion`, `edist_eval_le`, `edist_le`, `instBoundedSpace`, `isometry_restrict`, `lipschitzOnWith_iff`, `lipschitzWith_eval`, `lipschitzWith_iff`, `lipschitzWith_one_ofFun_toFun`, `lipschitzWith_one_ofFun_toFun'`, `lipschitzWith_restrict`	33
Total	41

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniformEquicontinuousOn` 📖	mathematical	`LipschitzOnWith`	`UniformEquicontinuousOn` `PseudoEMetricSpace.toUniformSpace`	—	`uniformEquicontinuousOn_iff_uniformContinuousOn` `uniformContinuousOn` `UniformFun.lipschitzOnWith_ofFun_iff`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniformEquicontinuous` 📖	mathematical	`LipschitzWith`	`UniformEquicontinuous` `PseudoEMetricSpace.toUniformSpace`	—	`uniformEquicontinuous_iff_uniformContinuous` `uniformContinuous` `UniformFun.lipschitzWith_ofFun_iff`

UniformFun

Definitions

Name	Category	Theorems
`instEDist` 📖	CompOp	6 math math: `edist_eval_le`, `edist_le`, `edist_def`, `UniformOnFun.edist_eq_pi_restrict`, `UniformOnFun.edist_eq_restrict_sUnion`, `edist_continuousMapMk`
`instEMetricSpace` 📖	CompOp	—
`instMetricSpaceOfBoundedSpace` 📖	CompOp	—
`instPseudoEMetricSpace` 📖	CompOp	10 math math: `UniformOnFun.isometry_restrict`, `UniformOnFun.lipschitzWith_one_ofFun_toFun`, `isometry_ofFun_continuousMap`, `isometry_ofFun_boundedContinuousFunction`, `lipschitzWith_ofFun_iff`, `lipschitzWith_iff`, `lipschitzOnWith_ofFun_iff`, `lipschitzOnWith_iff`, `UniformOnFun.lipschitzWith_restrict`, `lipschitzWith_eval`
`instPseudoMetricSpaceOfBoundedSpace` 📖	CompOp	3 math math: `instBoundedSpace`, `dist_le`, `dist_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_def` 📖	mathematical	—	`Dist.dist` `UniformFun` `PseudoMetricSpace.toDist` `instPseudoMetricSpaceOfBoundedSpace` `iSup` `Real` `Real.instSupSet` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`dist_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Dist.dist` `UniformFun` `PseudoMetricSpace.toDist` `instPseudoMetricSpaceOfBoundedSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	`dist_edist` `ENNReal.le_ofReal_iff_toReal_le` `edist_ne_top`
`edist_continuousMapMk` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	`EDist.edist` `ContinuousMap` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `ContinuousMap.instPseudoMetricSpace` `instEDist`	—	`Isometry.edist_eq` `isometry_ofFun_continuousMap`
`edist_def` 📖	mathematical	—	`EDist.edist` `UniformFun` `instEDist` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`edist_eval_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Equiv` `UniformFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instEDist`	—	`edist_le` `le_rfl`
`edist_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `UniformFun` `instEDist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	`iSup_le_iff`
`instBoundedSpace` 📖	mathematical	—	`BoundedSpace` `UniformFun` `PseudoMetricSpace.toBornology` `instPseudoMetricSpaceOfBoundedSpace`	—	`Metric.isBounded_iff_ediam_ne_top` `lt_top_iff_ne_top` `lt_of_le_of_lt` `Metric.edist_le_ediam_of_mem` `Set.mem_univ` `Ne.lt_top` `Bornology.IsBounded.ediam_ne_top` `BoundedSpace.bounded_univ`
`isometry_ofFun_boundedContinuousFunction` 📖	mathematical	—	`Isometry` `BoundedContinuousFunction` `UniformFun` `PseudoMetricSpace.toPseudoEMetricSpace` `BoundedContinuousFunction.instPseudoMetricSpace` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `BoundedContinuousFunction.instFunLike`	—	`BoundedContinuousFunction.edist_eq_iSup`
`isometry_ofFun_continuousMap` 📖	mathematical	—	`Isometry` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `UniformFun` `PseudoMetricSpace.toPseudoEMetricSpace` `ContinuousMap.instPseudoMetricSpace` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `ContinuousMap.instFunLike`	—	`Isometry.comp` `isometry_ofFun_boundedContinuousFunction` `IsometryEquiv.isometry`
`lipschitzOnWith_iff` 📖	mathematical	—	`LipschitzOnWith` `UniformFun` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`lipschitzOnWith_ofFun_iff` 📖	mathematical	—	`LipschitzOnWith` `UniformFun` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun`	—	`lipschitzOnWith_iff`
`lipschitzWith_eval` 📖	mathematical	—	`LipschitzWith` `UniformFun` `instPseudoEMetricSpace` `NNReal` `instOneNNReal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	`one_mul` `edist_eval_le`
`lipschitzWith_iff` 📖	mathematical	—	`LipschitzWith` `UniformFun` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`lipschitzWith_ofFun_iff` 📖	mathematical	—	`LipschitzWith` `UniformFun` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun`	—	`lipschitzWith_iff`

UniformOnFun

Definitions

Name	Category	Theorems
`instEDistOfFiniteElemSet` 📖	CompOp	8 math math: `edist_eval_le`, `edist_def'`, `edist_eq_pi_restrict`, `edist_def`, `edist_continuousRestrict`, `edist_eq_restrict_sUnion`, `edist_continuousRestrict_of_singleton`, `edist_le`
`instPseudoEMetricSpace` 📖	CompOp	11 math math: `isometry_restrict`, `lipschitzWith_one_ofFun_toFun`, `lipschitzOnWith_cfc_fun_of_subset`, `lipschitzWith_iff`, `lipschitzOnWith_cfc_fun`, `lipschitzOnWith_cfcₙ_fun`, `lipschitzWith_eval`, `lipschitzOnWith_iff`, `lipschitzOnWith_cfcₙ_fun_of_subset`, `lipschitzWith_restrict`, `lipschitzWith_one_ofFun_toFun'`
`instPseudoMetricSpaceOfBoundedSpace` 📖	CompOp	1 math math: `instBoundedSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_forall_lipschitzWith` 📖	mathematical	`LipschitzWith` `DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `topologicalSpace`	—	`continuous_rng_iff` `LipschitzWith.continuous` `UniformFun.lipschitzWith_iff`
`edist_continuousRestrict` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `Set.sUnion`	`EDist.edist` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `ContinuousMap.instPseudoMetricSpace` `Set.restrict` `ContinuousOn.restrict` `instEDistOfFiniteElemSet`	—	`ContinuousOn.restrict` `ContinuousMap.edist_eq_iSup` `iSup_subtype` `iSup_congr_Prop` `iSup_exists`
`edist_continuousRestrict_of_singleton` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `DFunLike.coe` `Equiv` `UniformOnFun` `Set` `Set.instSingletonSet` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	`EDist.edist` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `ContinuousMap.instPseudoMetricSpace` `Set.restrict` `ContinuousOn.restrict` `instEDistOfFiniteElemSet` `Finite.of_fintype` `Set.fintypeSingleton`	—	`ContinuousOn.restrict` `Finite.of_fintype` `ContinuousMap.edist_eq_iSup` `iSup_subtype` `iSup_congr_Prop` `Set.sUnion_singleton`
`edist_def` 📖	mathematical	—	`EDist.edist` `UniformOnFun` `instEDistOfFiniteElemSet` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `Set.sUnion` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`edist_def'` 📖	mathematical	—	`EDist.edist` `UniformOnFun` `instEDistOfFiniteElemSet` `iSup` `ENNReal` `Set` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instMembership` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	`iSup_congr_Prop` `iSup_exists` `iSup_and` `iSup_comm`
`edist_eq_pi_restrict` 📖	mathematical	—	`EDist.edist` `UniformOnFun` `instEDistOfFiniteElemSet` `Finite.of_fintype` `Set.Elem` `Set` `instEDistForall` `UniformFun` `Set.instMembership` `UniformFun.instEDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `Set.restrict` `toFun`	—	`Finite.of_fintype` `edist_def'` `iSup_congr_Prop` `iSup_subtype'` `Finset.sup_univ_eq_iSup`
`edist_eq_restrict_sUnion` 📖	mathematical	—	`EDist.edist` `UniformOnFun` `instEDistOfFiniteElemSet` `UniformFun` `Set.Elem` `Set.sUnion` `UniformFun.instEDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `Set.restrict` `toFun`	—	`iSup_subtype'`
`edist_eval_le` 📖	mathematical	`Set` `Set.instMembership` `Set.sUnion`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Equiv` `UniformOnFun` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun` `instEDistOfFiniteElemSet`	—	`edist_le` `le_rfl`
`edist_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `UniformOnFun` `instEDistOfFiniteElemSet` `PseudoEMetricSpace.toEDist` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`instBoundedSpace` 📖	mathematical	—	`BoundedSpace` `UniformOnFun` `PseudoMetricSpace.toBornology` `instPseudoMetricSpaceOfBoundedSpace`	—	`Set.ext` `Set.image_congr` `Set.image_univ` `LipschitzWith.isBounded_image` `lipschitzWith_one_ofFun_toFun` `Bornology.IsBounded.all` `UniformFun.instBoundedSpace`
`isometry_restrict` 📖	mathematical	—	`Isometry` `UniformOnFun` `Set` `Set.instSingletonSet` `UniformFun` `Set.Elem` `instPseudoEMetricSpace` `Finite.of_fintype` `Set.fintypeSingleton` `UniformFun.instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `Set.restrict` `toFun`	—	`Finite.of_fintype` `iSup_subtype` `iSup_congr_Prop` `Set.sUnion_singleton`
`lipschitzOnWith_iff` 📖	mathematical	—	`LipschitzOnWith` `UniformOnFun` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`lipschitzWith_eval` 📖	mathematical	`Set` `Set.instMembership` `Set.sUnion`	`LipschitzWith` `UniformOnFun` `instPseudoEMetricSpace` `NNReal` `instOneNNReal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	`one_mul` `edist_eval_le`
`lipschitzWith_iff` 📖	mathematical	—	`LipschitzWith` `UniformOnFun` `instPseudoEMetricSpace` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toFun`	—	—
`lipschitzWith_one_ofFun_toFun` 📖	mathematical	—	`LipschitzWith` `UniformFun` `UniformOnFun` `UniformFun.instPseudoEMetricSpace` `instPseudoEMetricSpace` `NNReal` `instOneNNReal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `UniformFun.toFun`	—	`lipschitzWith_iff` `UniformFun.lipschitzWith_eval`
`lipschitzWith_one_ofFun_toFun'` 📖	mathematical	`Set` `Set.instHasSubset` `Set.sUnion`	`LipschitzWith` `UniformOnFun` `instPseudoEMetricSpace` `NNReal` `instOneNNReal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofFun` `toFun`	—	`lipschitzWith_iff` `lipschitzWith_eval`
`lipschitzWith_restrict` 📖	mathematical	`Set` `Set.instMembership`	`LipschitzWith` `UniformOnFun` `UniformFun` `Set.Elem` `instPseudoEMetricSpace` `UniformFun.instPseudoEMetricSpace` `NNReal` `instOneNNReal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `UniformFun.ofFun` `Set.restrict` `toFun`	—	`UniformFun.lipschitzWith_iff` `lipschitzWith_eval`

---

← Back to Index