Mathlib v3 is deprecated. Go to Mathlib v4

Theorem absorbent.absorbs_finite

Modification history

2022-04-08 15:40

src/analysis/locally_convex/basic.lean

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

Added absorbent.absorbs_finite View on Github →