mathlib

69099f00 - feat(order/filter/bases): define `filter.has_basis` (#1896)

feat(order/filter/bases): define `filter.has_basis` (#1896) * feat(*): assorted simple lemmas, simplify some proofs * feat(order/filter/bases): define `filter.has_basis` * Add `@[nolint]` * +1 lemma, +1 simplified proof * Remove whitespaces Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Ref. note nolint_ge Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>