Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-08 15:40 05213440

View on Github →

feat(analysis/locally_convex/basic): add lemmas about finite unions for absorbs (#13236)

  • Lemma for absorbing sets and addition
  • Two Lemmas for absorbing sets as finite unions (set.finite and finset variant)
  • Lemma for absorbent sets absorb finite sets.

Estimated changes