Commit 2025-01-28 07:32 eff2ae8d

View on Github →

feat(Asymptotics): prove IsLittleOTVS.add (#20578)

Estimated changes

Modified Mathlib/Analysis/Asymptotics/TVS.lean

added theorem Asymptotics.IsLittleOTVS.add

Modified Mathlib/Analysis/Convex/EGauge.lean

added theorem egauge_add_add_le

Modified Mathlib/Order/Filter/SmallSets.lean

added theorem Filter.Eventually.exists_mem_basis_of_smallSets

added theorem Filter.Eventually.exists_mem_of_smallSets

added theorem Filter.Frequently.smallSets_of_forall_mem_basis

Modified Mathlib/Topology/Algebra/Monoid.lean

added theorem Filter.HasBasis.mul_self