Commit 2024-01-16 22:20 8bb0d697

View on Github →

refactor: redefine Absorbs (#9676) Redefine Absorbs and Absorbent in terms of the cobounded filter.

Estimated changes

deleted theorem Absorbent.absorbs
deleted theorem Absorbent.absorbs_finite
deleted theorem Absorbent.subset
added theorem Absorbent.zero_mem'
deleted theorem Absorbent.zero_mem
deleted def Absorbent
deleted theorem Absorbs.add
added theorem Absorbs.exists_pos
deleted theorem Absorbs.inter
deleted theorem Absorbs.mono
deleted theorem Absorbs.mono_left
deleted theorem Absorbs.mono_right
deleted theorem Absorbs.neg
deleted theorem Absorbs.sub
deleted theorem Absorbs.union
deleted def Absorbs
modified theorem Balanced.absorbs_self
deleted theorem Set.Finite.absorbs_iUnion
deleted theorem absorbent_iff_nonneg_lt
modified theorem absorbent_nhds_zero
deleted theorem absorbent_univ
deleted theorem absorbs_empty
deleted theorem absorbs_iUnion_finset
added theorem absorbs_iff_norm
deleted theorem absorbs_inter
deleted theorem absorbs_union
deleted theorem absorbs_zero_iff
added theorem Absorbent.vadd_absorbs
added theorem Absorbent.zero_mem
added def Absorbent
added theorem Absorbs.mono
added theorem Absorbs.mono_left
added theorem Absorbs.mono_right
added theorem Absorbs.sub
added def Absorbs
added theorem absorbent_iff_inv_smul
added theorem absorbent_univ
added theorem absorbs_biUnion_finset
added theorem absorbs_iInter
added theorem absorbs_iUnion
added theorem absorbs_inter
added theorem absorbs_neg_neg
added theorem absorbs_union
added theorem absorbs_zero_iff