Contractible

📁 Source: Mathlib/Analysis/Convex/Contractible.lean

Statistics

Metric	Count
Definitions	0
Theorems contractibleSpace, contractibleSpace, contractibleSpace	3
Total	3

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractibleSpace 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.Nonempty	ContractibleSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	StarConvex.contractibleSpace starConvex

RealTopologicalVectorSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractibleSpace 📖	mathematical	—	ContractibleSpace	—	Homeomorph.contractibleSpace_iff Convex.contractibleSpace convex_univ Set.univ_nonempty AddTorsor.nonempty

StarConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contractibleSpace 📖	mathematical	StarConvex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Set.Nonempty	ContractibleSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	contractible_iff_id_nullhomotopic mem Real.instZeroLEOneClass sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_sub_cancel Continuous.fun_add Continuous.smul Continuous.comp' continuous_subtype_val Continuous.fst continuous_id' continuous_const Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.snd Real.instIsOrderedRing zero_smul sub_zero one_smul zero_add Subtype.coe_eta sub_self add_zero

---

← Back to Index