Commit 2024-04-07 14:48 ab84fe13

View on Github →

feat(Topology/Algebra/StrongTopology): introduce type synonym for abstract topologies on CLM (#11470)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/LocallyConvex/StrongTopology.lean

deleted theorem ContinuousLinearMap.strongTopology.locallyConvexSpace

added theorem UniformConvergenceCLM.locallyConvexSpace

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

deleted theorem ContinuousLinearMap.strongTopology.continuousConstSMul

deleted theorem ContinuousLinearMap.strongTopology.continuousSMul

deleted theorem ContinuousLinearMap.strongTopology.embedding_coeFn

deleted theorem ContinuousLinearMap.strongTopology.hasBasis_nhds_zero

deleted theorem ContinuousLinearMap.strongTopology.hasBasis_nhds_zero_of_basis

deleted theorem ContinuousLinearMap.strongTopology.t2Space

deleted theorem ContinuousLinearMap.strongTopology.topologicalAddGroup

deleted theorem ContinuousLinearMap.strongTopology.uniformContinuousConstSMul

deleted def ContinuousLinearMap.strongTopology

deleted theorem ContinuousLinearMap.strongUniformity.uniformAddGroup

deleted theorem ContinuousLinearMap.strongUniformity.uniformEmbedding_coeFn

deleted def ContinuousLinearMap.strongUniformity

deleted theorem ContinuousLinearMap.strongUniformity_topology_eq

added theorem UniformConvergenceCLM.continuousSMul

added theorem UniformConvergenceCLM.embedding_coeFn

added theorem UniformConvergenceCLM.hasBasis_nhds_zero

added theorem UniformConvergenceCLM.hasBasis_nhds_zero_of_basis

added theorem UniformConvergenceCLM.t2Space

added theorem UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn

added theorem UniformConvergenceCLM.uniformEmbedding_coeFn

added theorem UniformConvergenceCLM.uniformity_toTopologicalSpace_eq

added def UniformConvergenceCLM