Theorem with_gaugeSeminormFamily

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