Mathlib Changelog
v3
Changelog
About
Github
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
Modified
docs/references.bib
Created
src/analysis/seminorm.lean
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
theorem
balanced_zero_union_interior
added
theorem
seminorm.balanced_ball_zero
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