PathConnected

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

Statistics

Metric	Count
Definitions segment	1
Theorems isConnected, isPathConnected, isPreconnected, pathConnectedSpace, of_segment_subset, cast_segment, eqOn_extend_segment, range_segment, segment_add_segment, segment_apply, segment_same, segment_symm, isPathConnected, isPathConnected, isPathConnected_compl_of_isPathConnected_compl_zero	15
Total	16

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected 📖	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	IsConnected	—	IsPathConnected.isConnected isPathConnected
isPathConnected 📖	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	IsPathConnected	—	StarConvex.isPathConnected
isPreconnected 📖	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	IsPreconnected	—	Set.eq_empty_or_nonempty isPreconnected_empty IsConnected.isPreconnected isConnected

IsTopologicalAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathConnectedSpace 📖	mathematical	—	PathConnectedSpace	—	pathConnectedSpace_iff_univ Convex.isPathConnected convex_univ

JoinedIn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_segment_subset 📖	mathematical	Set Set.instHasSubset segment 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	JoinedIn	—	Set.range_subset_iff Path.range_segment

Path

Definitions

Name	Category	Theorems
segment 📖	CompOp	19 math math: curveIntegrable_segment, curveIntegralFun_segment, norm_curveIntegral_segment_le, HasFDerivAt.curveIntegral_segment_source, curveIntegral_segment, curveIntegral_segment_const, segment_same, range_segment, Convex.curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric, segment_symm, HasFDerivWithinAt.curveIntegral_segment_source, HasFDerivAt.curveIntegral_segment_source', ContinuousMap.Homotopy.evalAt_affine, segment_add_segment, HasFDerivWithinAt.curveIntegral_segment_source', Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric, segment_apply, cast_segment, eqOn_extend_segment

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_segment 📖	mathematical	—	cast segment	—	—
eqOn_extend_segment 📖	mathematical	—	Set.EqOn Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend segment AffineMap Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap unitInterval	—	extend_apply
range_segment 📖	mathematical	—	Set.range Set.Elem Real unitInterval DFunLike.coe Path instFunLike segment segment 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	—	segment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.image_eq_range
segment_add_segment 📖	mathematical	—	add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid segment	—	ext AffineMap.lineMap_apply_module smul_add add_add_add_comm
segment_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike segment AffineMap Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddCommGroup.toAddGroup AffineMap.instFunLike AffineMap.lineMap Set Set.instMembership	—	—
segment_same 📖	mathematical	—	segment refl	—	ext AffineMap.lineMap_same
segment_symm 📖	mathematical	—	symm segment	—	ext AffineMap.lineMap_apply_one_sub

StarConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPathConnected 📖	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 Set.instMembership	IsPathConnected	—	JoinedIn.of_segment_subset segment_subset

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPathConnected 📖	mathematical	—	IsPathConnected SetLike.coe Submodule Real Real.semiring AddCommGroup.toAddCommMonoid setLike	—	Convex.isPathConnected convex nonempty

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPathConnected_compl_of_isPathConnected_compl_zero 📖	mathematical	IsCompl Submodule Real Real.semiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder CompleteLattice.toBoundedOrder Submodule.completeLattice IsPathConnected SetLike.instMembership Submodule.setLike instTopologicalSpaceSubtype Compl.compl Set Set.instCompl Set.instSingletonSet Submodule.zero	SetLike.coe	—	RingHomInvPair.ids Set.prod_univ LinearEquiv.image_eq_preimage_symm Set.ext IsCompl.symm Submodule.prodEquivOfIsCompl_symm_apply Set.image_congr IsPathConnected.add IsPathConnected.image continuous_subtype_val Submodule.isPathConnected

---

← Back to Index