Documentation Verification Report

BallSphere

📁 Source: Mathlib/Analysis/Normed/Group/BallSphere.lean

Statistics

Metric	Count
Definitions `instInvolutiveNegElemBallOfNat`, `instInvolutiveNegElemClosedBallOfNat`, `instInvolutiveNegElemSphereOfNat`	3
Theorems `coe_neg_ball`, `coe_neg_closedBall`, `coe_neg_sphere`, `instContinuousNegElemBallOfNat`, `instContinuousNegElemClosedBallOfNat`, `instContinuousNegElemSphereOfNat`	6
Total	9

(root)

Definitions

Name	Category	Theorems
`instInvolutiveNegElemBallOfNat` 📖	CompOp	2 math math: `instContinuousNegElemBallOfNat`, `coe_neg_ball`
`instInvolutiveNegElemClosedBallOfNat` 📖	CompOp	2 math math: `coe_neg_closedBall`, `instContinuousNegElemClosedBallOfNat`
`instInvolutiveNegElemSphereOfNat` 📖	CompOp	5 math math: `contMDiff_neg_sphere`, `coe_neg_sphere`, `stereographic_apply_neg`, `instContinuousNegElemSphereOfNat`, `stereographic_neg_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_neg_ball` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Set.Elem` `InvolutiveNeg.toNeg` `instInvolutiveNegElemBallOfNat` `NegZeroClass.toNeg`	—	—
`coe_neg_closedBall` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Set.Elem` `InvolutiveNeg.toNeg` `instInvolutiveNegElemClosedBallOfNat` `NegZeroClass.toNeg`	—	—
`coe_neg_sphere` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Set.Elem` `InvolutiveNeg.toNeg` `instInvolutiveNegElemSphereOfNat` `NegZeroClass.toNeg`	—	—
`instContinuousNegElemBallOfNat` 📖	mathematical	—	`ContinuousNeg` `Set.Elem` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `InvolutiveNeg.toNeg` `instInvolutiveNegElemBallOfNat`	—	`Topology.IsInducing.continuousNeg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Topology.IsInducing.subtypeVal`
`instContinuousNegElemClosedBallOfNat` 📖	mathematical	—	`ContinuousNeg` `Set.Elem` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `InvolutiveNeg.toNeg` `instInvolutiveNegElemClosedBallOfNat`	—	`Topology.IsInducing.continuousNeg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Topology.IsInducing.subtypeVal`
`instContinuousNegElemSphereOfNat` 📖	mathematical	—	`ContinuousNeg` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `InvolutiveNeg.toNeg` `instInvolutiveNegElemSphereOfNat`	—	`Topology.IsInducing.continuousNeg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Topology.IsInducing.subtypeVal`

---

← Back to Index