Commit 2025-05-12 15:03 9e281937

View on Github →

feat: define Path.segment (#24761) Extract the definition of Path.segment from JoinedIn.of_segment_subset and prove basic properties of this definition.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Convex.lean

Created Mathlib/Analysis/Convex/PathConnected.lean

added theorem JoinedIn.of_segment_subset

added theorem Path.cast_segment

added theorem Path.range_segment

added theorem Path.segment_add_segment

added theorem Submodule.isPathConnected

added theorem isPathConnected_compl_of_isPathConnected_compl_zero

Modified Mathlib/Analysis/Convex/Topology.lean

deleted theorem JoinedIn.of_segment_subset

deleted theorem Submodule.isPathConnected

deleted theorem isPathConnected_compl_of_isPathConnected_compl_zero

Modified Mathlib/Analysis/Normed/Module/Convex.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/Topology/Algebra/Module/LocallyConvex.lean