Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-14 22:08 05822370

View on Github →

feat(analysis): seminorms and local convexity (#4827)

Estimated changes

added def absorbent
added theorem absorbent_nhds_zero
added def absorbs
added theorem balanced.absorbs_self
added theorem balanced.closure
added theorem balanced.interior
added def balanced
added def seminorm.ball
added theorem seminorm.ball_zero_eq
added theorem seminorm.mem_ball
added theorem seminorm.mem_ball_zero
added theorem seminorm.nonneg
added theorem seminorm.sub_rev
added structure seminorm