Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 12:32 d01b55f1

View on Github →

split(analysis/functional/gauge): Split off analysis.seminorm (#12054) Move the Minkowski functional to a new file analysis.convex.gauge.

Estimated changes

added theorem balanced.star_convex
added theorem convex.gauge_le
added theorem exists_lt_of_gauge_lt
added def gauge
added theorem gauge_add_le
added theorem gauge_ball
added theorem gauge_def'
added theorem gauge_def
added theorem gauge_empty
added theorem gauge_le_eq
added theorem gauge_le_of_mem
added theorem gauge_le_one_of_mem
added theorem gauge_lt_eq'
added theorem gauge_lt_eq
added theorem gauge_lt_of_mem_smul
added theorem gauge_mono
added theorem gauge_neg
added theorem gauge_nonneg
added theorem gauge_of_subset_zero
added def gauge_seminorm
added theorem gauge_smul
added theorem gauge_smul_left
added theorem gauge_smul_of_nonneg
added theorem gauge_unit_ball
added theorem gauge_zero'
added theorem gauge_zero
added theorem le_gauge_of_not_mem
added theorem mul_gauge_le_norm
added theorem smul_unit_ball
deleted theorem balanced.star_convex
deleted theorem convex.gauge_le
deleted theorem exists_lt_of_gauge_lt
deleted def gauge
deleted theorem gauge_add_le
deleted theorem gauge_ball
deleted theorem gauge_def'
deleted theorem gauge_def
deleted theorem gauge_empty
deleted theorem gauge_le_eq
deleted theorem gauge_le_of_mem
deleted theorem gauge_le_one_of_mem
deleted theorem gauge_lt_eq'
deleted theorem gauge_lt_eq
deleted theorem gauge_lt_of_mem_smul
deleted theorem gauge_lt_one_subset_self
deleted theorem gauge_mono
deleted theorem gauge_neg
deleted theorem gauge_nonneg
deleted theorem gauge_of_subset_zero
deleted def gauge_seminorm
deleted theorem gauge_smul
deleted theorem gauge_smul_left
deleted theorem gauge_smul_left_of_nonneg
deleted theorem gauge_smul_of_nonneg
deleted theorem gauge_unit_ball
deleted theorem gauge_zero'
deleted theorem gauge_zero
deleted theorem le_gauge_of_not_mem
deleted theorem mul_gauge_le_norm
deleted theorem one_le_gauge_of_not_mem
deleted theorem self_subset_gauge_le_one
deleted theorem smul_unit_ball