Documentation Verification Report

EuclideanDist

📁 Source: Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean

Statistics

Metric	Count
Definitions `ball`, `closedBall`, `dist`, `toEuclidean`	4
Theorems `euclidean_dist`, `ball_eq_preimage`, `ball_mem_nhds`, `ball_subset_closedBall`, `closedBall_eq_image`, `closedBall_eq_preimage`, `closedBall_mem_nhds`, `closure_ball`, `exists_pos_lt_subset_ball`, `isClosed_closedBall`, `isCompact_closedBall`, `isOpen_ball`, `mem_ball_self`, `nhds_basis_ball`, `nhds_basis_closedBall`	15
Total	19

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`euclidean_dist` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop.some` `ENat`	`Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Euclidean.dist` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NormedSpace.toModule` `Real.normedField` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `dist` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `comp` `ContinuousLinearEquiv.contDiff` `ContinuousLinearEquiv.injective`

Euclidean

Definitions

Name	Category	Theorems
`ball` 📖	CompOp	7 math math: `mem_ball_self`, `ball_mem_nhds`, `isOpen_ball`, `ball_subset_closedBall`, `nhds_basis_ball`, `ball_eq_preimage`, `closure_ball`
`closedBall` 📖	CompOp	8 math math: `closedBall_eq_image`, `nhds_basis_closedBall`, `isCompact_closedBall`, `ball_subset_closedBall`, `closedBall_eq_preimage`, `closedBall_mem_nhds`, `closure_ball`, `isClosed_closedBall`
`dist` 📖	CompOp	1 math math: `ContDiff.euclidean_dist`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_eq_preimage` 📖	mathematical	—	`ball` `Set.preimage` `EuclideanSpace` `Real` `Module.finrank` `Real.semiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Real.instRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `toEuclidean` `Metric.ball` `PiLp.instPseudoMetricSpace`	—	—
`ball_mem_nhds` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Filter` `Filter.instMembership` `nhds` `ball`	—	`Filter.HasBasis.mem_of_mem` `nhds_basis_ball`
`ball_subset_closedBall` 📖	mathematical	—	`Set` `Set.instHasSubset` `ball` `closedBall`	—	`le_of_lt`
`closedBall_eq_image` 📖	mathematical	—	`closedBall` `Set.image` `EuclideanSpace` `Real` `Module.finrank` `Real.semiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Real.instRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `toEuclidean` `Metric.closedBall` `PiLp.instPseudoMetricSpace`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `ContinuousLinearEquiv.image_symm_eq_preimage` `closedBall_eq_preimage`
`closedBall_eq_preimage` 📖	mathematical	—	`closedBall` `Set.preimage` `EuclideanSpace` `Real` `Module.finrank` `Real.semiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `Real.normedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Real.instRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `toEuclidean` `Metric.closedBall` `PiLp.instPseudoMetricSpace`	—	—
`closedBall_mem_nhds` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Filter` `Filter.instMembership` `nhds` `closedBall`	—	`Filter.HasBasis.mem_of_mem` `nhds_basis_closedBall`
`closure_ball` 📖	mathematical	—	`closure` `ball` `closedBall`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `ball_eq_preimage` `ContinuousLinearEquiv.preimage_closure` `closure_ball` `closedBall_eq_preimage`
`exists_pos_lt_subset_ball` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instHasSubset` `ball`	`Set.instMembership` `Set.Ioo` `Real.instPreorder`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `exists_pos_lt_subset_ball` `FiniteDimensional.proper_real` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `ContinuousLinearEquiv.isClosed_image` `Set.image_subset_iff` `ball_eq_preimage`
`isClosed_closedBall` 📖	mathematical	—	`IsClosed` `closedBall`	—	`IsCompact.isClosed` `isCompact_closedBall`
`isCompact_closedBall` 📖	mathematical	—	`IsCompact` `closedBall`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `closedBall_eq_image` `IsCompact.image` `ProperSpace.isCompact_closedBall` `FiniteDimensional.proper_real` `WithLp.instModuleFinite` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `ContinuousLinearEquiv.continuous`
`isOpen_ball` 📖	mathematical	—	`IsOpen` `ball`	—	`IsOpen.preimage` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `ContinuousLinearEquiv.continuous` `Metric.isOpen_ball`
`mem_ball_self` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `ball`	—	`Metric.mem_ball_self` `fact_one_le_two_ennreal` `RingHomInvPair.ids`
`nhds_basis_ball` 📖	mathematical	—	`Filter.HasBasis` `Real` `nhds` `Real.instLT` `Real.instZero` `ball`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Homeomorph.nhds_eq_comap` `Filter.HasBasis.comap` `Metric.nhds_basis_ball`
`nhds_basis_closedBall` 📖	mathematical	—	`Filter.HasBasis` `Real` `nhds` `Real.instLT` `Real.instZero` `closedBall`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Homeomorph.nhds_eq_comap` `Filter.HasBasis.comap` `Metric.nhds_basis_closedBall`

(root)

Definitions

Name	Category	Theorems
`toEuclidean` 📖	CompOp	3 math math: `Euclidean.closedBall_eq_image`, `Euclidean.closedBall_eq_preimage`, `Euclidean.ball_eq_preimage`

---

← Back to Index