Documentation Verification Report

Sphere

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

Statistics

Metric	Count
Definitions `ball`, `ballInclusion`, `disk`, `diskBoundary`, `diskBoundaryInclusion`, `sphere`, `term𝔹_`, `term𝔻_`, `term𝕊_`, `«term∂𝔻_»`	10
Theorems `instCompactSpaceCarrierDisk`, `instCompactSpaceCarrierDiskBoundary`, `instMonoBallInclusion`, `instMonoDiskBoundaryInclusion`	4
Total	14

TopCat

Definitions

Name	Category	Theorems
`ball` 📖	CompOp	1 math math: `instMonoBallInclusion`
`ballInclusion` 📖	CompOp	1 math math: `instMonoBallInclusion`
`disk` 📖	CompOp	3 math math: `instMonoBallInclusion`, `instMonoDiskBoundaryInclusion`, `instCompactSpaceCarrierDisk`
`diskBoundary` 📖	CompOp	2 math math: `instCompactSpaceCarrierDiskBoundary`, `instMonoDiskBoundaryInclusion`
`diskBoundaryInclusion` 📖	CompOp	1 math math: `instMonoDiskBoundaryInclusion`
`sphere` 📖	CompOp	—
`term𝔹_` 📖	CompOp	—
`term𝔻_` 📖	CompOp	—
`term𝕊_` 📖	CompOp	—
`«term∂𝔻_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompactSpaceCarrierDisk` 📖	mathematical	—	`CompactSpace` `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` 📖	mathematical	—	`CompactSpace` `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` 📖	mathematical	—	`CategoryTheory.Mono` `TopCat` `instCategory` `ball` `disk` `ballInclusion`	—	`mono_iff_injective` `fact_one_le_two_ennreal`
`instMonoDiskBoundaryInclusion` 📖	mathematical	—	`CategoryTheory.Mono` `TopCat` `instCategory` `diskBoundary` `disk` `diskBoundaryInclusion`	—	`mono_iff_injective` `fact_one_le_two_ennreal`

---

← Back to Index