Theorem Absorbent.subset_range_iff_surjective

Modification history

2025-12-27 09:40
Mathlib/Analysis/LocallyConvex/Basic.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified Absorbent.subset_range_iff_surjectiveView on Github →
2025-11-07 20:33
Mathlib/Analysis/LocallyConvex/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 Absorbent.subset_range_iff_surjectiveView on Github →