Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-29 19:42 f798f22e

View on Github →

refactor(order/filter/bases): drop p in has_antitone_basis (#10499) We never use has_antitone_basis for p ≠ λ _, true in mathlib.

Estimated changes

Modified src/order/filter/at_top_bot.lean

modified theorem filter.subseq_tendsto_of_ne_bot

Modified src/order/filter/bases.lean

deleted theorem filter.exists_antitone_eq_infi_principal

modified structure filter.has_antitone_basis

modified structure filter.is_antitone_basis

Modified src/topology/G_delta.lean

Modified src/topology/sequences.lean

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/cauchy.lean