Commit 2022-07-09 01:15 c5b6fe54

View on Github →

feat(analysis/locally_convex/basic): a few lemmas about balanced sets (#14876) Add new lemmas about unions and intersection and membership of balanced sets.

Estimated changes

Modified src/analysis/locally_convex/basic.lean

modified theorem absorbs.add

added theorem absorbs.neg

added theorem absorbs.sub

modified theorem absorbs_Union_finset

modified theorem balanced.add

added theorem balanced.mem_smul_iff

added theorem balanced.neg

added theorem balanced.neg_mem_iff

modified theorem balanced.smul

added theorem balanced.sub

added theorem balanced_Inter

added theorem balanced_Inter₂

added theorem balanced_Union

added theorem balanced_Union₂

added theorem balanced_empty

modified theorem balanced_univ

modified theorem set.finite.absorbs_Union