Commit 2025-09-27 14:30 63fd0cfe

View on Github →

refactor(Analysis/LocallyConvex/WithSeminorms): Relax some of the hypothesis (#29604) Relax some of the hypothesis in Analysis/LocallyConvex/WithSeminorms

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

modified theorem Seminorm.continuous_iff_continuous_comp

modified def SeminormFamily.basisSets

modified theorem SeminormFamily.basisSets_smul_left

modified theorem SeminormFamily.filter_eq_iInf