Theorem Seminorm.neg_mem_ball_zero

Modification history

2024-01-31 09:33
Mathlib/Analysis/Seminorm.lean
chore(Analysis/Seminorm): make statement of `neg_mem_ball_zero` iff (#10119)
Modified Seminorm.neg_mem_ball_zeroView on Github →
2024-01-16 14:21
Mathlib/Analysis/Seminorm.lean
chore(Analysis,Geometry): remove almost all autoImplicit (#9691) …
Modified Seminorm.neg_mem_ball_zeroView on Github →
2023-07-13 11:32
Mathlib/Analysis/Seminorm.lean
feat(Analysis.Seminorm, Analysis.LocallyConvex.WithSeminorms): minimize some assumptions (#5812)
Added Seminorm.neg_mem_ball_zeroView on Github →