Commit 2024-05-17 23:45 b9e4edd6

View on Github →

feat(Analysis/EGauge): new file (#12852) Define egauge, needed to define Fréchet derivative for functions between topological vector spaces.

Estimated changes

added theorem div_le_egauge_ball
added theorem egauge_anti
added theorem egauge_empty
added theorem egauge_eq_top
added theorem egauge_le_of_mem_smul
added theorem egauge_le_of_smul_mem
added theorem egauge_le_one
added theorem egauge_lt_iff
added theorem egauge_smul_left
added theorem egauge_smul_right
added theorem egauge_zero_right
added theorem egauge_zero_zero
added theorem le_egauge_ball_one
added theorem le_egauge_iff
added theorem le_egauge_smul_left
added theorem le_egauge_smul_right
added theorem mem_of_egauge_lt_one
added theorem NNReal.nnnorm_eq_self