Theorem AbsConvexOpenSets.coe_isOpen

Modification history

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_isOpenView on Github →
2023-05-25 08:46
Mathlib/Analysis/LocallyConvex/AbsConvex.lean
feat: port Analysis.LocallyConvex.AbsConvex (#4320)
Added AbsConvexOpenSets.coe_isOpenView on Github →