Commit 2026-03-11 00:21 f2b7f455

View on Github →

chore: Seminorm.continuous_from_bounded -> WithSeminorms.continuous_of_isBounded (#36397)

Estimated changes

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

Modified Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean

Modified Mathlib/Analysis/LocallyConvex/WeakDual.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

deleted theorem Seminorm.cont_normedSpace_to_withSeminorms

deleted theorem Seminorm.cont_withSeminorms_normedSpace

deleted theorem Seminorm.continuous_from_bounded

deleted theorem Seminorm.continuous_iff_continuous_comp

deleted theorem Seminorm.continuous_of_continuous_comp

added theorem WithSeminorms.continuous_iff_continuous_comp

added theorem WithSeminorms.continuous_normedSpace_dom

added theorem WithSeminorms.continuous_normedSpace_rng

added theorem WithSeminorms.continuous_of_continuous_comp

added theorem WithSeminorms.continuous_of_isBounded

modified theorem WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup

modified theorem WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm