Theorem AbsConvexOpenSets.coe_convex

Modification history

2025-10-14 23:03
Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean
refactor(Analysis/LocallyConvex/AbsConvex): Redefine AbsConvex to use a single ring of scalars (#29342) …
Modified AbsConvexOpenSets.coe_convexView on Github →
2025-02-17 21:24
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
refactor(Analysis/LocallyConvex/AbsConvexOpen): Break out AbsConvexOpenSets into its own file (#21928) …
Modified AbsConvexOpenSets.coe_convexView on Github →
2023-05-25 08:46
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
feat: port Analysis.LocallyConvex.AbsConvex (#4320)
Added AbsConvexOpenSets.coe_convexView on Github →