Commit 2024-01-30 14:33 7f0ee211

View on Github →

feat(Gauge): add comap_gauge_nhds_zero etc (#10090) Add comap_gauge_nhds_zero, comap_gauge_nhds_zero_le, tendsto_gauge_nhds_zero, tendsto_gauge_nhds_zero', and continuousAt_gauge_zero.

Estimated changes

Modified Mathlib/Analysis/Convex/Gauge.lean

added theorem comap_gauge_nhds_zero

added theorem comap_gauge_nhds_zero_le

added theorem continuousAt_gauge_zero

modified theorem gauge_eq_zero

modified theorem gauge_pos

added theorem tendsto_gauge_nhds_zero'

added theorem tendsto_gauge_nhds_zero