Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-17 10:21 c46f021f

View on Github →

feat(analysis/seminorm): characterize continuity of seminorms by closed balls (#17249)

Estimated changes

Modified src/analysis/locally_convex/with_seminorms.lean

modified theorem seminorm.cont_normed_space_to_with_seminorms

modified theorem seminorm.cont_with_seminorms_normed_space

modified theorem seminorm.continuous_from_bounded

modified theorem seminorm.continuous_iff_continuous_comp

modified theorem seminorm.continuous_of_continuous_comp

modified theorem with_seminorms.continuous_seminorm

Modified src/analysis/seminorm.lean

added theorem seminorm.ball_norm_mul_subset

added theorem seminorm.continuous_at_zero'

modified theorem seminorm.continuous_at_zero

modified theorem seminorm.continuous_of_le

added theorem seminorm.restrict_scalars_closed_ball

added theorem seminorm.smul_closed_ball_subset

added theorem seminorm.smul_closed_ball_zero