Theorem gauge_pos

Modification history

2024-01-30 14:33

Mathlib/Analysis/Convex/Gauge.lean

feat(Gauge): add `comap_gauge_nhds_zero` etc (#10090) …

Modified gauge_pos View on Github →

2023-07-24 10:30

Mathlib/Analysis/Convex/Gauge.lean

feat: expand/review API about `gauge` (#5321)

Added gauge_pos View on Github →