Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 13:35 b21c1c9b

View on Github →

split(analysis/locally_convex/basic): Split off analysis.seminorm (#12624) Move balanced, absorbs, absorbent to a new file. For analysis.seminorm, I'm crediting

Estimated changes

added theorem absorbent.absorbs
added theorem absorbent.subset
added theorem absorbent.zero_mem
added def absorbent
added theorem absorbent_nhds_zero
added theorem absorbent_univ
added theorem absorbs.inter
added theorem absorbs.mono
added theorem absorbs.mono_left
added theorem absorbs.mono_right
added theorem absorbs.union
added def absorbs
added theorem absorbs_inter
added theorem absorbs_union
added theorem absorbs_zero_iff
added theorem balanced.absorbs_self
added theorem balanced.add
added theorem balanced.closure
added theorem balanced.inter
added theorem balanced.interior
added theorem balanced.smul
added theorem balanced.smul_eq
added theorem balanced.smul_mono
added theorem balanced.subset_smul
added theorem balanced.union
added def balanced
added theorem balanced_univ
deleted theorem absorbent.absorbs
deleted theorem absorbent.subset
deleted theorem absorbent.zero_mem
deleted def absorbent
deleted theorem absorbent_iff_nonneg_lt
deleted theorem absorbent_nhds_zero
deleted theorem absorbent_univ
deleted theorem absorbs.inter
deleted theorem absorbs.mono
deleted theorem absorbs.mono_left
deleted theorem absorbs.mono_right
deleted theorem absorbs.union
deleted def absorbs
deleted theorem absorbs_inter
deleted theorem absorbs_union
deleted theorem absorbs_zero_iff
deleted theorem balanced.absorbs_self
deleted theorem balanced.add
deleted theorem balanced.closure
deleted theorem balanced.inter
deleted theorem balanced.interior
deleted theorem balanced.smul
deleted theorem balanced.smul_eq
deleted theorem balanced.smul_mono
deleted theorem balanced.subset_smul
deleted theorem balanced.union
deleted def balanced
deleted theorem balanced_univ