Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-21 08:15 ae9b867e

View on Github →

feat(analysis/seminorm): continuity criterion for seminorms (#16402)

Estimated changes

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

added theorem abs_sub_map_le_div

Modified src/analysis/seminorm.lean

added theorem seminorm.continuous_at_zero

added theorem seminorm.continuous_of_le

added theorem seminorm.mem_ball_self

added theorem seminorm.norm_sub_map_le_sub