Commit 2023-07-13 11:32 929a09b7

View on Github →

feat(Analysis.Seminorm, Analysis.LocallyConvex.WithSeminorms): minimize some assumptions (#5812)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

modified theorem SeminormFamily.withSeminorms_iff_nhds_eq_iInf

modified theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf

modified theorem SeminormFamily.withSeminorms_of_hasBasis

modified theorem SeminormFamily.withSeminorms_of_nhds

added theorem WithSeminorms.continuousSMul

modified theorem WithSeminorms.continuous_seminorm

Modified Mathlib/Analysis/Seminorm.lean

added theorem Seminorm.continuousAt_zero_of_forall'

added theorem Seminorm.continuousAt_zero_of_forall

modified theorem Seminorm.continuous_of_le

added theorem Seminorm.neg_mem_ball_zero

deleted theorem Seminorm.symmetric_ball_zero