Theorem AbsConvexOpenSets.coe_nhds

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_nhds View on Github →

2023-05-25 08:46

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

feat: port Analysis.LocallyConvex.AbsConvex (#4320)

Added AbsConvexOpenSets.coe_nhds View on Github →