Documentation Verification Report

RadialEquiv

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

Statistics

Metric	Count
Definitions `homeomorphSphereProd`, `homeomorphUnitSphereProd`	2
Theorems `smul_sphere`, `homeomorphSphereProd_apply_fst_coe`, `homeomorphSphereProd_apply_snd_coe`, `homeomorphSphereProd_symm_apply_coe`, `homeomorphUnitSphereProd_apply_fst_coe`, `homeomorphUnitSphereProd_apply_snd_coe`, `homeomorphUnitSphereProd_symm_apply_coe`	7
Total	9

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_sphere` 📖	mathematical	`IsOpen` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Set.instMembership` `Real.instZero` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `instTopologicalSpaceSubtype`	`Set.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Set.image`	—	`isOpen_iff_mem_nhds` `lt_of_le_of_ne` `norm_eq_of_mem_sphere` `norm_nonneg` `CanLift.prf` `Subtype.canLift` `prod_mem_nhds` `mem_nhds` `preimage_val` `Filter.image_mem_map` `Filter.mp_mem` `homeomorphSphereProd_symm_apply_coe` `nhdsWithin_eq` `isOpen_compl_singleton` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `LT.lt.ne'` `Membership.mem.out` `map_nhds_subtype_val` `Homeomorph.map_nhds_eq` `Filter.map_map` `Filter.univ_mem'` `Set.smul_mem_smul` `Set.mem_image_of_mem` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_iff_eq_or_lt` `not_lt` `neg_neg` `neg_smul` `nhds_neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Set.neg_smul` `neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `neg_zero`

(root)

Definitions

Name	Category	Theorems
`homeomorphSphereProd` 📖	CompOp	3 math math: `homeomorphSphereProd_symm_apply_coe`, `homeomorphSphereProd_apply_snd_coe`, `homeomorphSphereProd_apply_fst_coe`
`homeomorphUnitSphereProd` 📖	CompOp	5 math math: `MeasureTheory.Measure.toSphere_apply_aux`, `homeomorphUnitSphereProd_symm_apply_coe`, `MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd`, `homeomorphUnitSphereProd_apply_fst_coe`, `homeomorphUnitSphereProd_apply_snd_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homeomorphSphereProd_apply_fst_coe` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Set.Elem` `Set.Ioi` `Real.instPreorder` `DFunLike.coe` `Homeomorph` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceProd` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphSphereProd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm`	—	—
`homeomorphSphereProd_apply_snd_coe` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `Set.Ioi` `Real.instPreorder` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `Homeomorph` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceProd` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphSphereProd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	—
`homeomorphSphereProd_symm_apply_coe` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `Homeomorph` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.Ioi` `Real.instPreorder` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeomorphSphereProd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	—
`homeomorphUnitSphereProd_apply_fst_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `Set.Elem` `Set.Ioi` `Real.instPreorder` `Real.instZero` `DFunLike.coe` `Homeomorph` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceProd` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphUnitSphereProd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`one_smul`
`homeomorphUnitSphereProd_apply_snd_coe` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instOne` `DFunLike.coe` `Homeomorph` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instTopologicalSpaceProd` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphUnitSphereProd` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`div_one`
`homeomorphUnitSphereProd_symm_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Compl.compl` `Set.instCompl` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `Homeomorph` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real` `Real.instOne` `Set.Ioi` `Real.instPreorder` `Real.instZero` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeomorphUnitSphereProd` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	—

---

← Back to Index