Commit 2023-07-24 10:30 a888c045

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/Convex/Gauge.lean

added theorem Convex.lipschitz_gauge

added theorem continuous_gauge

added theorem gauge_ball'

modified theorem gauge_ball

added theorem gauge_closedBall

added theorem gauge_closure_zero

added theorem gauge_eq_one_iff_mem_frontier

added theorem gauge_eq_zero

added theorem gauge_le_one_iff_mem_closure

added theorem gauge_lt_one_eq_interior

added theorem gauge_lt_one_iff_mem_interior

added theorem gauge_pos

modified theorem gauge_unit_ball

added theorem le_gauge_of_subset_closedBall

added theorem mem_closure_of_gauge_le_one

added theorem mem_frontier_of_gauge_eq_one

added theorem mem_openSegment_of_gauge_lt_one