Theorem Submodule.Convex.semilinear_range

Modification history

2025-11-07 20:33
Mathlib/Analysis/Convex/Basic.lean
feat(Analysis.LocallyConvex): a linear map is surjective iff its image contains a ball, or a closed ball, or a sphere (#29033) …
Added Submodule.Convex.semilinear_rangeView on Github →