Documentation Verification Report

PathComponentOne

📁 Source: Mathlib/Topology/Connected/PathComponentOne.lean

Statistics

Metric	Count
Definitions `pathComponentZero`, `pathComponentOne`	2
Theorems `instIsClosedCoePathComponentZero`, `pathComponentZero_carrier`, `instIsClosedCoePathComponentOne`, `pathComponentOne_carrier`	4
Total	6

OpenNormalAddSubgroup

Definitions

Name	Category	Theorems
`pathComponentZero` 📖	CompOp	2 math math: `instIsClosedCoePathComponentZero`, `pathComponentZero_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedCoePathComponentZero` 📖	mathematical	—	`IsClosed` `SetLike.coe` `OpenNormalAddSubgroup` `instSetLike` `pathComponentZero`	—	`IsClosed.pathComponent`
`pathComponentZero_carrier` 📖	mathematical	—	`SetLike.coe` `OpenNormalAddSubgroup` `instSetLike` `pathComponentZero` `pathComponent` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—

OpenNormalSubgroup

Definitions

Name	Category	Theorems
`pathComponentOne` 📖	CompOp	2 math math: `instIsClosedCoePathComponentOne`, `pathComponentOne_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedCoePathComponentOne` 📖	mathematical	—	`IsClosed` `SetLike.coe` `OpenNormalSubgroup` `instSetLike` `pathComponentOne`	—	`IsClosed.pathComponent`
`pathComponentOne_carrier` 📖	mathematical	—	`SetLike.coe` `OpenNormalSubgroup` `instSetLike` `pathComponentOne` `pathComponent` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—

---

← Back to Index