Documentation Verification Report

Homeomorph

📁 Source: Mathlib/Analysis/Normed/Module/Ball/Homeomorph.lean

Statistics

Metric	Count
Definitions `unitBall`, `unitBallBall`, `univBall`, `univUnitBall`	4
Theorems `coe_unitBall_apply_zero`, `unitBall_apply_coe`, `unitBall_symm_apply`, `ball_subset_univBall_target`, `continuousOn_univBall_symm`, `continuous_univBall`, `unitBallBall_apply`, `unitBallBall_source`, `unitBallBall_symm_apply`, `unitBallBall_target`, `univBall_apply_zero`, `univBall_source`, `univBall_symm_apply_center`, `univBall_target`, `univUnitBall_apply`, `univUnitBall_apply_zero`, `univUnitBall_source`, `univUnitBall_symm_apply`, `univUnitBall_symm_apply_zero`, `univUnitBall_target`	20
Total	24

Homeomorph

Definitions

Name	Category	Theorems
`unitBall` 📖	CompOp	4 math math: `contDiff_unitBall`, `coe_unitBall_apply_zero`, `unitBall_apply_coe`, `unitBall_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_unitBall_apply_zero` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `DFunLike.coe` `Homeomorph` `Set.Elem` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `instEquivLike` `unitBall`	—	`OpenPartialHomeomorph.univUnitBall_apply_zero`
`unitBall_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `DFunLike.coe` `Homeomorph` `Set.Elem` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `instEquivLike` `unitBall` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.univUnitBall`	—	—
`unitBall_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Set.Elem` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `unitBall` `Set.univ` `OpenPartialHomeomorph.toHomeomorphSourceTarget` `OpenPartialHomeomorph.univUnitBall`	—	—

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
`unitBallBall` 📖	CompOp	6 math math: `contDiff_unitBallBall_symm`, `unitBallBall_target`, `contDiff_unitBallBall`, `unitBallBall_source`, `unitBallBall_symm_apply`, `unitBallBall_apply`
`univBall` 📖	CompOp	9 math math: `continuousOn_univBall_symm`, `continuous_univBall`, `univBall_apply_zero`, `contDiff_univBall`, `contDiffOn_univBall_symm`, `ball_subset_univBall_target`, `univBall_target`, `univBall_symm_apply_center`, `univBall_source`
`univUnitBall` 📖	CompOp	10 math math: `univUnitBall_symm_apply_zero`, `univUnitBall_apply_zero`, `contDiff_univUnitBall`, `univUnitBall_target`, `contDiffOn_univUnitBall_symm`, `univUnitBall_source`, `Homeomorph.unitBall_apply_coe`, `univUnitBall_apply`, `univUnitBall_symm_apply`, `Homeomorph.unitBall_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_subset_univBall_target` 📖	mathematical	—	`Set` `Set.instHasSubset` `Metric.ball` `PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univBall`	—	`univBall_target` `subset_refl` `Set.instReflSubset` `univBall.eq_1` `Set.subset_univ`
`continuousOn_univBall_symm` 📖	mathematical	—	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toFun'` `symm` `univBall` `Metric.ball`	—	`ContinuousOn.mono` `continuousOn` `ball_subset_univBall_target`
`continuous_univBall` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toFun'` `univBall`	—	`univBall_source` `continuousOn`
`unitBallBall_apply` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `unitBallBall` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `NormedAddTorsor.toAddTorsor` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Module.toDistribMulAction` `DivisionSemiring.toSemiring` `NormedSpace.toModule` `Real.normedField`	—	—
`unitBallBall_source` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`PartialEquiv.source` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `unitBallBall` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real.instOne`	—	—
`unitBallBall_symm_apply` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `symm` `unitBallBall` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Module.toDistribMulAction` `DivisionSemiring.toSemiring` `NormedSpace.toModule` `Real.normedField` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `VSub.vsub` `AddTorsor.toVSub` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddTorsor.toAddTorsor`	—	—
`unitBallBall_target` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `unitBallBall` `Metric.ball`	—	—
`univBall_apply_zero` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`univUnitBall_apply_zero` `smul_zero` `zero_vadd`
`univBall_source` 📖	mathematical	—	`PartialEquiv.source` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univBall` `Set.univ`	—	—
`univBall_symm_apply_center` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `symm` `univBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`univBall_source` `univBall_apply_zero` `left_inv`
`univBall_target` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univBall` `Metric.ball`	—	`univBall.eq_1`
`univUnitBall_apply` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univUnitBall` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Real.sqrt` `Real.instAdd` `Real.instOne` `Monoid.toNatPow` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	—
`univUnitBall_apply_zero` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univUnitBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_zero` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `add_zero` `Real.sqrt_one` `inv_one` `smul_zero`
`univUnitBall_source` 📖	mathematical	—	`PartialEquiv.source` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univUnitBall` `Set.univ`	—	—
`univUnitBall_symm_apply` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `symm` `univUnitBall` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Real.sqrt` `Real.instSub` `Real.instOne` `Monoid.toNatPow` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	—
`univUnitBall_symm_apply_zero` 📖	mathematical	—	`toFun'` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `symm` `univUnitBall` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_zero` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `sub_zero` `Real.sqrt_one` `inv_one` `smul_zero`
`univUnitBall_target` 📖	mathematical	—	`PartialEquiv.target` `toPartialEquiv` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `univUnitBall` `Metric.ball` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne`	—	—

---

← Back to Index