Commit 2023-08-31 11:52 23550c1e

View on Github →

feat: the complement of a countable set is path-connected in dimension > 1 (#6690) Also show that spheres are path-connected in dimension > 1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Segment.lean

added theorem segment_inter_eq_endpoint_of_linearIndependent_of_ne

added theorem segment_inter_eq_endpoint_of_linearIndependent_sub

Modified Mathlib/Analysis/Convex/Topology.lean

added theorem JoinedIn_of_segment_subset

Created Mathlib/Analysis/NormedSpace/Connected.lean

added theorem Set.Countable.isConnected_compl_of_one_lt_rank

added theorem Set.Countable.isPathConnected_compl_of_one_lt_rank

added theorem isConnected_compl_singleton_of_one_lt_rank

added theorem isConnected_sphere

added theorem isPathConnected_compl_singleton_of_one_lt_rank

added theorem isPathConnected_sphere

added theorem isPreconnected_sphere

Modified Mathlib/Data/Set/Countable.lean

added theorem Set.countable_setOf_nonempty_of_disjoint

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added theorem LinearIndependent.eq_zero_of_pair'

added theorem LinearIndependent.linear_combination_pair_of_det_ne_zero

added theorem LinearIndependent.pair_iff