Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 10:50 247943a9

View on Github →

feat(analysis/seminorm): add inf (#11791) Define the infimum of seminorms.

Estimated changes

Modified src/analysis/seminorm.lean

added theorem seminorm.inf_apply

added theorem seminorm.le_insert'

added theorem seminorm.le_insert

added theorem seminorm.smul_inf

Modified src/order/conditionally_complete_lattice.lean

added theorem csupr_mul_csupr_le

added theorem csupr_mul_le

added theorem le_cinfi_mul

added theorem le_cinfi_mul_cinfi

added theorem le_mul_cinfi

added theorem mul_csupr_le