Commit 2024-02-11 13:33 750e6f24

View on Github →

feat(LocallyConvex/Bounded): add IsVonNBounded.add etc (#10135)

add IsVonNBounded.add, IsVonNBounded.vadd, and isVonNBounded_vadd;
generalize some lemmas in Topology/Algebra/Monoid from Monoid to MulOneClass, move them to a new section.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

added theorem Bornology.IsVonNBounded.of_add_left

added theorem Bornology.IsVonNBounded.of_add_right

added theorem Bornology.IsVonNBounded.of_sub_left

added theorem Bornology.IsVonNBounded.of_sub_right

added theorem Bornology.isVonNBounded_add

added theorem Bornology.isVonNBounded_add_of_nonempty

added theorem Bornology.isVonNBounded_add_self

added theorem Bornology.isVonNBounded_neg

added theorem Bornology.isVonNBounded_sub

added theorem Bornology.isVonNBounded_sub_of_nonempty

added theorem Bornology.isVonNBounded_vadd

Modified Mathlib/Data/Finset/Pointwise.lean

added theorem Finset.inv_eq_empty

Modified Mathlib/Data/Set/Pointwise/Basic.lean

added theorem Set.inv_eq_empty

Modified Mathlib/Topology/Algebra/Monoid.lean