Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-26 12:57 8edffc25

View on Github →

feat(order/filter/bases): lemmas about bases of product filters (#15630)

  • Move has_basis.prod_self and mem_prod_self_iff down to golf the proof.
  • Rename has_basis.prod'' to has_basis.prod_pprod.
  • Rename has_basis.prod' to has_basis.prod_same_index.
  • Add has_basis.prod_same_index_mono and has_basis.prod_same_index_anti.

Estimated changes

deleted theorem filter.has_basis.prod''
deleted theorem filter.has_basis.prod'
modified theorem filter.has_basis.prod_self
modified theorem filter.mem_prod_self_iff