Commit 2024-09-17 02:57 ab21cb1b

View on Github →

feat: define Filter.absorbing (#15215) Also prove that a set is von Neumann bounded iff Filter.absorbing 𝕜 S ≤ 𝓝 0. These lemmas make it easy to simplify IsVonNBounded 𝕜 S, provided that we have 𝓝 0 = ⨅ (a1 a2 ... ak), 𝓟 (f a1 a2 ... ak), even if the family of sets in the RHS is not directed, so Filter.HasBasis is false.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

added theorem Bornology.isVonNBounded_iff_absorbing_le

Modified Mathlib/Topology/Bornology/Absorbs.lean

added def Filter.absorbing

added theorem Filter.mem_absorbing

modified theorem Set.Finite.absorbs_biInter

modified theorem Set.Finite.absorbs_sInter

modified theorem absorbs_iInter

modified theorem absorbs_iff_eventually_cobounded_mapsTo

modified theorem absorbs_inter

modified theorem absorbs_zero_iff