Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 18:05 fd4a034d

View on Github →

refactor(analysis/locally_convex/with_seminorms): use abbreviations to allow for dot notation (#12846)

Estimated changes

Modified src/analysis/locally_convex/with_seminorms.lean

modified theorem seminorm.continuous_from_bounded

deleted def seminorm_add_group_filter_basis

deleted def seminorm_basis_zero

deleted theorem seminorm_basis_zero_add

deleted theorem seminorm_basis_zero_iff

deleted theorem seminorm_basis_zero_intersect

deleted theorem seminorm_basis_zero_mem

deleted theorem seminorm_basis_zero_neg

deleted theorem seminorm_basis_zero_nonempty

deleted theorem seminorm_basis_zero_singleton_mem

deleted theorem seminorm_basis_zero_smul

deleted theorem seminorm_basis_zero_smul_left

deleted theorem seminorm_basis_zero_smul_right

deleted theorem seminorm_basis_zero_zero

added def seminorm_family.basis_sets

added theorem seminorm_family.basis_sets_add

added theorem seminorm_family.basis_sets_iff

added theorem seminorm_family.basis_sets_intersect

added theorem seminorm_family.basis_sets_mem

added theorem seminorm_family.basis_sets_neg

added theorem seminorm_family.basis_sets_nonempty

added theorem seminorm_family.basis_sets_singleton_mem

added theorem seminorm_family.basis_sets_smul

added theorem seminorm_family.basis_sets_smul_left

added theorem seminorm_family.basis_sets_smul_right

added theorem seminorm_family.basis_sets_zero

added theorem seminorm_family.to_locally_convex_space

added theorem seminorm_family.with_seminorms_eq

added theorem seminorm_family.with_seminorms_of_has_basis

added theorem seminorm_family.with_seminorms_of_nhds

added def seminorm_family

deleted def seminorm_module_filter_basis

deleted theorem with_seminorms.to_locally_convex_space

deleted theorem with_seminorms_eq

deleted theorem with_seminorms_of_has_basis

deleted theorem with_seminorms_of_nhds