Commit 2022-01-31 19:55 750f53c8

View on Github →

feat(analysis/seminorm): define the topology induced by a family of seminorms (#11604) Define the topology induced by a single seminorm and by a family of seminorms and show that boundedness of linear maps implies continuity.

Estimated changes

Modified src/analysis/seminorm.lean

modified theorem seminorm.ball_finset_sup

modified theorem seminorm.ball_finset_sup_eq_Inter

added theorem seminorm.ball_smul

added theorem seminorm.const_is_bounded

added theorem seminorm.cont_normed_space_to_with_seminorms

added theorem seminorm.cont_with_seminorms_normed_space

added theorem seminorm.continuous_from_bounded

added theorem seminorm.finset_sup_le_sum

added def seminorm.is_bounded

added theorem seminorm.is_bounded_const

added theorem seminorm.is_bounded_sup

added def seminorm.pullback

added def seminorm.seminorm_add_group_filter_basis

added def seminorm.seminorm_basis_zero

added theorem seminorm.seminorm_basis_zero_add

added theorem seminorm.seminorm_basis_zero_iff

added theorem seminorm.seminorm_basis_zero_intersect

added theorem seminorm.seminorm_basis_zero_mem

added theorem seminorm.seminorm_basis_zero_neg

added theorem seminorm.seminorm_basis_zero_nonempty

added theorem seminorm.seminorm_basis_zero_singleton_mem

added theorem seminorm.seminorm_basis_zero_smul

added theorem seminorm.seminorm_basis_zero_smul_left

added theorem seminorm.seminorm_basis_zero_smul_right

added theorem seminorm.seminorm_basis_zero_zero

added def seminorm.seminorm_module_filter_basis

added theorem seminorm.smul_le_smul

added theorem seminorm.with_seminorms_eq