mathlib

f798f22e - refactor(order/filter/bases): drop `p` in `has_antitone_basis` (#10499)

refactor(order/filter/bases): drop `p` in `has_antitone_basis` (#10499) We never use `has_antitone_basis` for `p ≠ λ _, true` in `mathlib`. Co-authored-by: Patrick Massot <patrickmassot@free.fr>