Commit 2022-09-09 12:28 3a0b839b

View on Github →

feat(analysis/{normed/group}/seminorm): Hom classes for seminorms (#16227) Introduce add_group_seminorm_class, group_seminorm_class, seminorm_class, the hom classes of add_group_seminorm, group_seminorm, seminorm.

Estimated changes

Modified counterexamples/seminorm_lattice_not_distrib.lean

Modified src/algebra/order/absolute_value.lean

Created src/algebra/order/hom/basic.lean

added theorem le_map_add_map_div

Modified src/analysis/convex/gauge.lean

Modified src/analysis/locally_convex/with_seminorms.lean

Modified src/analysis/normed/group/seminorm.lean

modified theorem group_seminorm.comp_zero

deleted theorem group_seminorm.div_rev

modified theorem group_seminorm.ext

deleted theorem group_seminorm.le_insert'

deleted theorem group_seminorm.le_insert

added theorem le_map_add_map_div'

added theorem map_div_le_add

added theorem map_div_rev

Modified src/analysis/seminorm.lean

added theorem seminorm.bdd_below_range_add

deleted theorem seminorm.le_insert'

deleted theorem seminorm.le_insert

modified def seminorm.pullback

deleted theorem seminorm.sub_rev