Theorem gaugeSeminormFamily_ball

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

2023-05-25 08:46

Mathlib/Analysis/LocallyConvex/AbsConvex.lean

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

Added gaugeSeminormFamily_ball View on Github →