Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-21 00:16 d71cab9f

View on Github →

feat(analysis/seminorm): add composition with linear maps (#11477) This PR defines the composition of seminorms with linear maps and shows that composition is monotone and calculates the seminorm ball of the composition.

Estimated changes

added theorem seminorm.add_comp
added theorem seminorm.ball_comp
added theorem seminorm.coe_comp
added def seminorm.comp
added theorem seminorm.comp_apply
added theorem seminorm.comp_comp
added theorem seminorm.comp_id
added theorem seminorm.comp_mono
added theorem seminorm.comp_smul
added theorem seminorm.comp_triangle
added theorem seminorm.comp_zero
added theorem seminorm.smul_comp
added theorem seminorm.zero_apply
added theorem seminorm.zero_comp