Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-05 17:02 b916d59f

View on Github →

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology (#16053)

Estimated changes

Modified src/analysis/convolution.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/analysis/normed_space/multilinear.lean

Modified src/analysis/normed_space/operator_norm.lean

Created src/topology/algebra/module/strong_topology.lean

added theorem continuous_linear_map.strong_topology.has_basis_nhds_zero

added theorem continuous_linear_map.strong_topology.has_basis_nhds_zero_of_basis

added theorem continuous_linear_map.strong_topology.has_continuous_smul

added theorem continuous_linear_map.strong_topology.topological_add_group

added def continuous_linear_map.strong_topology

added theorem continuous_linear_map.strong_uniformity.uniform_add_group

added def continuous_linear_map.strong_uniformity

added theorem continuous_linear_map.strong_uniformity_topology_eq

Modified src/topology/vector_bundle/hom.lean

modified def topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change

modified theorem topological_vector_bundle.pretrivialization.continuous_linear_map_coord_change_apply

modified theorem topological_vector_bundle.pretrivialization.continuous_on_continuous_linear_map_coord_change