Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-07 07:07 559f58b1

View on Github →

feat(order/filter): add a few lemmas (#13985)

  • weaken assumptions of filter.has_antitone_basis.tendsto from [semilattice_sup ι] [nonempty ι] to [preorder ι];
  • add filter.has_antitone_basis.tendsto, filter.has_antitone_basis.mem, filter.has_antitone_basis.tendsto_small_sets.

Estimated changes