Mathlib v3 is deprecated. Go to Mathlib v4

Theorem seminorm.le_insert'

Modification history

2022-09-09 12:28
src/analysis/seminorm.lean
feat(analysis/{normed/group}/seminorm): Hom classes for seminorms (#16227) …
Deleted seminorm.le_insert'View on Github →
2022-06-09 13:27
src/analysis/seminorm.lean
feat(analysis/seminorm): removed unnecessary `norm_one_class` arguments (#14614)
Modified seminorm.le_insert'View on Github →
2022-02-22 10:50
src/analysis/seminorm.lean
feat(analysis/seminorm): add inf (#11791) …
Added seminorm.le_insert'View on Github →