Contractible

📁 Source: Mathlib/Topology/Homotopy/Contractible.lean

Statistics

Metric	Count
Definitions Nullhomotopic, ContractibleSpace	2
Theorems contractibleSpace, contractibleSpace_iff, comp_left, comp_right, nullhomotopic_of_constant, hequiv, hequiv_unit, hequiv_unit', instOfNonemptyOfSubsingleton, instPathConnectedSpace, instProd, contractibleSpace, contractibleSpace_iff, contractible_iff_id_nullhomotopic, id_nullhomotopic	15
Total	17

ContinuousMap

Definitions

Name	Category	Theorems
Nullhomotopic 📖	MathDef	3 math math: contractible_iff_id_nullhomotopic, nullhomotopic_of_constant, id_nullhomotopic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nullhomotopic_of_constant 📖	mathematical	—	Nullhomotopic const	—	Homotopic.refl

ContinuousMap.HomotopyEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractibleSpace 📖	mathematical	—	ContractibleSpace	—	Nonempty.map ContractibleSpace.hequiv_unit
contractibleSpace_iff 📖	mathematical	—	ContractibleSpace	—	contractibleSpace

ContinuousMap.Nullhomotopic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left 📖	mathematical	ContinuousMap.Nullhomotopic	ContinuousMap.comp	—	ContinuousMap.Homotopic.comp ContinuousMap.Homotopic.refl
comp_right 📖	mathematical	ContinuousMap.Nullhomotopic	ContinuousMap.comp	—	ContinuousMap.Homotopic.comp ContinuousMap.Homotopic.refl

ContractibleSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hequiv 📖	mathematical	—	ContinuousMap.HomotopyEquiv	—	hequiv_unit'
hequiv_unit 📖	mathematical	—	ContinuousMap.HomotopyEquiv instTopologicalSpacePUnit	—	hequiv_unit'
hequiv_unit' 📖	mathematical	—	ContinuousMap.HomotopyEquiv instTopologicalSpacePUnit	—	—
instOfNonemptyOfSubsingleton 📖	mathematical	—	ContractibleSpace	—	nonempty_unique
instPathConnectedSpace 📖	mathematical	—	PathConnectedSpace	—	id_nullhomotopic pathConnectedSpace_iff_eq Set.ext
instProd 📖	mathematical	—	ContractibleSpace instTopologicalSpaceProd	—	hequiv_unit'

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractibleSpace 📖	mathematical	—	ContractibleSpace	—	ContinuousMap.HomotopyEquiv.contractibleSpace
contractibleSpace_iff 📖	mathematical	—	ContractibleSpace	—	ContinuousMap.HomotopyEquiv.contractibleSpace_iff

(root)

Definitions

Name	Category	Theorems
ContractibleSpace 📖	CompData	19 math math: Metric.contractibleSpace_ball, StarConvex.contractibleSpace, Homeomorph.contractibleSpace, Metric.contractibleSpace_closedBall, ContractibleSpace.instProd, Homeomorph.contractibleSpace_iff, StronglyLocallyContractibleSpace.contractible_basis, contractible_subset_basis, ContinuousMap.HomotopyEquiv.contractibleSpace, UpperHalfPlane.instContractibleSpace, contractible_iff_id_nullhomotopic, Convex.contractibleSpace, ContinuousMap.HomotopyEquiv.contractibleSpace_iff, RealTopologicalVectorSpace.contractibleSpace, Metric.contractibleSpace_eball, ContractibleSpace.instOfNonemptyOfSubsingleton, Metric.eball_contractible, Metric.contractibleSpace_closedEBall, Metric.ball_contractible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractible_iff_id_nullhomotopic 📖	mathematical	—	ContractibleSpace ContinuousMap.Nullhomotopic ContinuousMap.id	—	id_nullhomotopic ContinuousMap.Homotopic.symm ContinuousMap.Homotopic.refl
id_nullhomotopic 📖	mathematical	—	ContinuousMap.Nullhomotopic ContinuousMap.id	—	ContractibleSpace.hequiv_unit ContinuousMap.Homotopic.symm ContinuousMap.HomotopyEquiv.left_inv

---

← Back to Index