Theorem AmpleSet.of_one_lt_codim

Modification history

2025-02-16 15:19
Mathlib/Analysis/Convex/AmpleSet.lean
chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)
Modified AmpleSet.of_one_lt_codimView on Github →
2024-06-06 16:20
Mathlib/Analysis/Convex/AmpleSet.lean
feat: complements of codimension at least two subspaces are ample (#11342) …
Added AmpleSet.of_one_lt_codimView on Github →