Commit 2025-11-07 20:33 7b709925

View on Github →

feat(Analysis.LocallyConvex): a linear map is surjective iff its image contains a ball, or a closed ball, or a sphere (#29033) Prove that a linear map is surjective if and only if its image contains either a ball or a sphere.

Estimated changes

Modified Mathlib/Analysis/Convex/Basic.lean

added theorem Convex.semilinear_image

added theorem Submodule.Convex.semilinear_range

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

added theorem Absorbent.eq_univ_of_smulMemClass

added theorem Absorbent.submodule_eq_top

added theorem Absorbent.subset_range_iff_surjective

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

added theorem convexHull_sphere_eq_closedBall

Modified Mathlib/Analysis/Normed/Operator/Basic.lean

added theorem ball_subset_range_iff_surjective

added theorem ball_zero_subset_range_iff_surjective

added theorem closedBall_subset_range_iff_surjective

added theorem sphere_subset_range_iff_surjective