Commit 2025-08-07 13:16 f405d4f8

View on Github →

chore: remove Nonempty assumptions in WithSeminorms (#27874)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/Analysis/LocallyConvex/WeakDual.lean

Modified Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

modified theorem LinearMap.withSeminorms_induced

modified theorem Seminorm.bound_of_continuous

modified theorem SeminormFamily.basisSets_nonempty

added theorem SeminormFamily.basisSets_univ_mem

modified theorem Topology.IsInducing.withSeminorms

modified theorem withSeminorms_iInf