Documentation Verification Report

SimplyConnected

📁 Source: Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

Statistics

Metric	Count
Definitions `IsSimplyConnected`, `SimplyConnectedSpace`	2
Theorems `simplyConnectedSpace`, `simplyConnectedSpace_iff`, `isSimplyConnected_image`, `isSimplyConnected_preimage`, `isPathConnected`, `nonempty`, `simplyConnectedSpace`, `equiv_unit`, `instPathConnectedSpace`, `instSubsingletonQuotient`, `ofContractible`, `paths_homotopic`, `isSimplyConnected_image`, `isSimplyConnected_iff_exists_homotopy_refl_forall_mem`, `isSimplyConnected_smul_set_iff`, `isSimplyConnected_smul_set₀_iff`, `isSimplyConnected_vadd_set_iff`, `simplyConnectedSpace_iff`, `simply_connected_def`, `simply_connected_iff_loops_nullhomotopic`, `simply_connected_iff_paths_homotopic`, `simply_connected_iff_paths_homotopic'`, `simply_connected_iff_unique_homotopic`	23
Total	25

ContinuousMap.HomotopyEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`simplyConnectedSpace` 📖	mathematical	—	`SimplyConnectedSpace`	—	`Nonempty.map` `SimplyConnectedSpace.equiv_unit`
`simplyConnectedSpace_iff` 📖	mathematical	—	`SimplyConnectedSpace`	—	`simplyConnectedSpace`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimplyConnected_image` 📖	mathematical	—	`IsSimplyConnected` `Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`Topology.IsEmbedding.isSimplyConnected_image` `isEmbedding`
`isSimplyConnected_preimage` 📖	mathematical	—	`IsSimplyConnected` `Set.preimage` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `isSimplyConnected_image`

IsSimplyConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPathConnected` 📖	mathematical	—	`IsPathConnected`	—	`simplyConnectedSpace` `isPathConnected_iff_pathConnectedSpace` `SimplyConnectedSpace.instPathConnectedSpace`
`nonempty` 📖	mathematical	—	`Set.Nonempty`	—	`IsPathConnected.nonempty` `isPathConnected`
`simplyConnectedSpace` 📖	mathematical	—	`SimplyConnectedSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	—

SimplyConnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_unit` 📖	mathematical	—	`CategoryTheory.Equivalence` `FundamentalGroupoid` `CategoryTheory.Discrete` `CategoryTheory.Groupoid.toCategory` `FundamentalGroupoid.instGroupoid` `CategoryTheory.discreteCategory`	—	—
`instPathConnectedSpace` 📖	mathematical	—	`PathConnectedSpace`	—	`simply_connected_iff_unique_homotopic`
`instSubsingletonQuotient` 📖	mathematical	—	`Path.Homotopic.Quotient`	—	`Unique.instSubsingleton` `simply_connected_iff_unique_homotopic`
`ofContractible` 📖	mathematical	—	`SimplyConnectedSpace`	—	`ContinuousMap.HomotopyEquiv.simplyConnectedSpace` `ContractibleSpace.hequiv` `ContractibleSpace.instOfNonemptyOfSubsingleton`
`paths_homotopic` 📖	mathematical	—	`Path.Homotopic`	—	`Quotient.eq` `instSubsingletonQuotient`

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimplyConnected_image` 📖	mathematical	`Topology.IsEmbedding`	`IsSimplyConnected` `Set.image`	—	`ContinuousMap.HomotopyEquiv.simplyConnectedSpace_iff`

(root)

Definitions

Name	Category	Theorems
`IsSimplyConnected` 📖	MathDef	7 math math: `Topology.IsEmbedding.isSimplyConnected_image`, `Homeomorph.isSimplyConnected_image`, `isSimplyConnected_vadd_set_iff`, `isSimplyConnected_smul_set_iff`, `isSimplyConnected_smul_set₀_iff`, `Homeomorph.isSimplyConnected_preimage`, `isSimplyConnected_iff_exists_homotopy_refl_forall_mem`
`SimplyConnectedSpace` 📖	CompData	10 math math: `simply_connected_def`, `simply_connected_iff_unique_homotopic`, `IsSimplyConnected.simplyConnectedSpace`, `simply_connected_iff_paths_homotopic`, `ContinuousMap.HomotopyEquiv.simplyConnectedSpace`, `simplyConnectedSpace_iff`, `ContinuousMap.HomotopyEquiv.simplyConnectedSpace_iff`, `simply_connected_iff_loops_nullhomotopic`, `SimplyConnectedSpace.ofContractible`, `simply_connected_iff_paths_homotopic'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSimplyConnected_iff_exists_homotopy_refl_forall_mem` 📖	mathematical	—	`IsSimplyConnected` `IsPathConnected` `Set` `Set.instMembership` `DFunLike.coe` `Path.Homotopy` `Path.refl` `Set.Elem` `Real` `unitInterval` `ContinuousMap.HomotopyWith.instFunLike` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Path.toContinuousMap`	—	`Real.instIsOrderedRing` `IsSimplyConnected.eq_1` `simply_connected_iff_loops_nullhomotopic` `isPathConnected_iff_pathConnectedSpace` `Iff.and` `CanLift.prf` `Subtype.canLift` `Path.source` `ContinuousMapClass.map_continuous` `Path.continuousMapClass` `Subtype.coe_eta` `Path.target` `continuous_subtype_val` `ContinuousMap.HomotopyLike.toContinuousMapClass` `ContinuousMap.HomotopyWith.instHomotopyLike` `ContinuousMap.HomotopyWith.apply_zero` `Path.map_coe` `ContinuousMap.HomotopyWith.apply_one` `Path.Homotopy.source` `Path.Homotopy.target`
`isSimplyConnected_smul_set_iff` 📖	mathematical	—	`IsSimplyConnected` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Homeomorph.isSimplyConnected_image`
`isSimplyConnected_smul_set₀_iff` 📖	mathematical	—	`IsSimplyConnected` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulAction.toSemigroupAction`	—	`isSimplyConnected_smul_set_iff` `Units.continuousConstSMul`
`isSimplyConnected_vadd_set_iff` 📖	mathematical	—	`IsSimplyConnected` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Homeomorph.isSimplyConnected_image`
`simplyConnectedSpace_iff` 📖	mathematical	—	`SimplyConnectedSpace` `CategoryTheory.Equivalence` `FundamentalGroupoid` `CategoryTheory.Discrete` `CategoryTheory.Groupoid.toCategory` `FundamentalGroupoid.instGroupoid` `CategoryTheory.discreteCategory`	—	—
`simply_connected_def` 📖	mathematical	—	`SimplyConnectedSpace` `CategoryTheory.Equivalence` `FundamentalGroupoid` `CategoryTheory.Discrete` `CategoryTheory.Groupoid.toCategory` `FundamentalGroupoid.instGroupoid` `CategoryTheory.discreteCategory`	—	`simplyConnectedSpace_iff`
`simply_connected_iff_loops_nullhomotopic` 📖	mathematical	—	`SimplyConnectedSpace` `PathConnectedSpace` `Path.Homotopic` `Path.refl`	—	`simply_connected_iff_paths_homotopic'` `Path.Homotopic.Quotient.eq` `Path.Homotopic.Quotient.trans_assoc` `Path.Homotopic.Quotient.symm_trans` `Path.Homotopic.Quotient.trans_refl`
`simply_connected_iff_paths_homotopic` 📖	mathematical	—	`SimplyConnectedSpace` `PathConnectedSpace` `Path.Homotopic.Quotient`	—	`SimplyConnectedSpace.instPathConnectedSpace` `SimplyConnectedSpace.instSubsingletonQuotient` `simply_connected_iff_unique_homotopic` `ConnectedSpace.toNonempty` `PathConnectedSpace.connectedSpace`
`simply_connected_iff_paths_homotopic'` 📖	mathematical	—	`SimplyConnectedSpace` `PathConnectedSpace` `Path.Homotopic`	—	`simply_connected_iff_paths_homotopic`
`simply_connected_iff_unique_homotopic` 📖	mathematical	—	`SimplyConnectedSpace` `Unique` `Path.Homotopic.Quotient`	—	`FundamentalGroupoid.nonempty_iff`

---

← Back to Index