Documentation Verification Report

Bordism

📁 Source: Mathlib/Geometry/Manifold/Bordism.lean

Statistics

Metric	Count
Definitions `SingularManifold`, `chartedSpace`, `comap`, `empty`, `f`, `instChartedSpaceM`, `instTopologicalSpaceM`, `map`, `prod`, `refl`, `sum`, `toPUnit`, `topSpaceM`	13
Theorems `boundaryless`, `comap_M`, `comap_f`, `compactSpace`, `empty_M`, `hf`, `instBoundarylessManifoldRealM`, `instCompactSpaceM`, `instIsEmptyMEmpty`, `instIsManifoldRealM`, `isManifold`, `map_M`, `map_comp`, `map_f`, `sum_M`, `sum_f`	16
Total	29

SingularManifold

Definitions

Name	Category	Theorems
`chartedSpace` 📖	CompOp	2 math math: `isManifold`, `boundaryless`
`comap` 📖	CompOp	2 math math: `comap_f`, `comap_M`
`empty` 📖	CompOp	2 math math: `empty_M`, `instIsEmptyMEmpty`
`f` 📖	CompOp	5 math math: `comap_f`, `sum_f`, `map_f`, `map_comp`, `hf`
`instChartedSpaceM` 📖	CompOp	2 math math: `instBoundarylessManifoldRealM`, `instIsManifoldRealM`
`instTopologicalSpaceM` 📖	CompOp	3 math math: `instCompactSpaceM`, `instBoundarylessManifoldRealM`, `instIsManifoldRealM`
`map` 📖	CompOp	3 math math: `map_f`, `map_comp`, `map_M`
`prod` 📖	CompOp	—
`refl` 📖	CompOp	—
`sum` 📖	CompOp	2 math math: `sum_f`, `sum_M`
`toPUnit` 📖	CompOp	—
`topSpaceM` 📖	CompOp	4 math math: `isManifold`, `boundaryless`, `compactSpace`, `hf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundaryless` 📖	mathematical	—	`BoundarylessManifold` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `M` `topSpaceM` `chartedSpace`	—	—
`comap_M` 📖	mathematical	`Continuous` `M` `instTopologicalSpaceM`	`comap`	—	—
`comap_f` 📖	mathematical	`Continuous` `M` `instTopologicalSpaceM`	`f` `comap`	—	—
`compactSpace` 📖	mathematical	—	`CompactSpace` `M` `topSpaceM`	—	—
`empty_M` 📖	mathematical	—	`M` `empty`	—	—
`hf` 📖	mathematical	—	`Continuous` `M` `topSpaceM` `f`	—	—
`instBoundarylessManifoldRealM` 📖	mathematical	—	`BoundarylessManifold` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `M` `instTopologicalSpaceM` `instChartedSpaceM`	—	`boundaryless`
`instCompactSpaceM` 📖	mathematical	—	`CompactSpace` `M` `instTopologicalSpaceM`	—	`compactSpace`
`instIsEmptyMEmpty` 📖	mathematical	—	`IsEmpty` `M` `empty`	—	`IsEmpty.false`
`instIsManifoldRealM` 📖	mathematical	—	`IsManifold` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `M` `instTopologicalSpaceM` `instChartedSpaceM`	—	`isManifold`
`isManifold` 📖	mathematical	—	`IsManifold` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `M` `topSpaceM` `chartedSpace`	—	—
`map_M` 📖	mathematical	`Continuous`	`M` `map`	—	—
`map_comp` 📖	mathematical	`Continuous`	`f` `map` `M`	—	—
`map_f` 📖	mathematical	`Continuous`	`f` `map` `M`	—	—
`sum_M` 📖	mathematical	—	`M` `sum`	—	—
`sum_f` 📖	mathematical	—	`f` `sum` `M`	—	—

(root)

Definitions

Name	Category	Theorems
`SingularManifold` 📖	CompData	—

---

← Back to Index