Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 11:17 2a6fef39

View on Github →

refactor(order/filter/bases): allow ι : Sort* (#8856)

  • ι in filter.has_basis (l : filter α) (p : ι → Prop) (s : ι → set ) now can be a Sort *;
  • some lemmas now have "primed" versions that use pprod instead of prod;
  • new lemma: filter.has_basis_supr. I also added a few missing lemmas to data.pprod and golfed a couple of proofs.

Estimated changes

added theorem pprod.exists'
added theorem pprod.forall'
modified theorem pprod.mk.eta
added theorem pprod.«exists»
added theorem pprod.«forall»
modified structure filter.has_antimono_basis
added theorem filter.has_basis.inf'
modified theorem filter.has_basis.inf
modified theorem filter.has_basis.prod
added theorem filter.has_basis.sup'
modified theorem filter.has_basis.sup
added theorem filter.has_basis_supr
modified structure filter.is_antimono_basis