Documentation Verification Report

Sphere

📁 Source: Mathlib/Topology/Category/TopCat/Sphere.lean

Statistics

MetricCount
Definitionsball, ballInclusion, disk, diskBoundary, diskBoundaryInclusion, sphere, term𝔹_, term𝔻_, term𝕊_, «term∂𝔻_»
10
TheoremsinstCompactSpaceCarrierDisk, instCompactSpaceCarrierDiskBoundary, instMonoBallInclusion, instMonoDiskBoundaryInclusion
4
Total14

TopCat

Definitions

NameCategoryTheorems
ball 📖CompOp
1 mathmath: instMonoBallInclusion
ballInclusion 📖CompOp
1 mathmath: instMonoBallInclusion
disk 📖CompOp
3 mathmath: instMonoBallInclusion, instMonoDiskBoundaryInclusion, instCompactSpaceCarrierDisk
diskBoundary 📖CompOp
2 mathmath: instCompactSpaceCarrierDiskBoundary, instMonoDiskBoundaryInclusion
diskBoundaryInclusion 📖CompOp
1 mathmath: instMonoDiskBoundaryInclusion
sphere 📖CompOp
term𝔹_ 📖CompOp
term𝔻_ 📖CompOp
term𝕊_ 📖CompOp
«term∂𝔻_» 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
instCompactSpaceCarrierDisk 📖mathematicalCompactSpace
carrier
disk
str
fact_one_le_two_ennreal
Homeomorph.compactSpace
instCompactSpaceElemClosedBallOfProperSpace
FiniteDimensional.proper_real
WithLp.instModuleFinite
FiniteDimensional.finiteDimensional_pi'
Finite.of_fintype
FiniteDimensional.rclike_to_real
instCompactSpaceCarrierDiskBoundary 📖mathematicalCompactSpace
carrier
diskBoundary
str
fact_one_le_two_ennreal
Homeomorph.compactSpace
Metric.sphere.compactSpace
FiniteDimensional.proper_real
WithLp.instModuleFinite
FiniteDimensional.finiteDimensional_pi'
Finite.of_fintype
FiniteDimensional.rclike_to_real
instMonoBallInclusion 📖mathematicalCategoryTheory.Mono
TopCat
instCategory
ball
disk
ballInclusion
mono_iff_injective
fact_one_le_two_ennreal
instMonoDiskBoundaryInclusion 📖mathematicalCategoryTheory.Mono
TopCat
instCategory
diskBoundary
disk
diskBoundaryInclusion
mono_iff_injective
fact_one_le_two_ennreal

---

← Back to Index