Commit 2022-07-19 23:27 cfc157d3

View on Github →

chore(analysis/locally_convex/with_seminorms): change with_seminorms to a structure (#15388) Change the class with_seminorms into a structure. The typeclass was useless in the first case since it can be only infered in trivial cases. Now it is somehow similar to how has_basis behaves.

Estimated changes

Modified src/analysis/locally_convex/weak_dual.lean

added theorem linear_map.weak_bilin_with_seminorms

Modified src/analysis/locally_convex/with_seminorms.lean

deleted theorem bornology.is_vonN_bounded_iff_finset_seminorm_bounded

modified theorem bornology.is_vonN_bounded_iff_seminorm_bounded

added theorem norm_with_seminorms

modified theorem seminorm.continuous_from_bounded

deleted theorem seminorm_family.has_basis

modified theorem seminorm_family.to_locally_convex_space

modified theorem seminorm_family.with_seminorms_eq

added theorem with_seminorms.has_basis

added theorem with_seminorms.is_vonN_bounded_iff_finset_seminorm_bounded

added structure with_seminorms