mathlib3

2d9f791d - feat(order/filter): add lemmas about filter.has_antitone_basis (#14131)

feat(order/filter): add lemmas about filter.has_antitone_basis (#14131) * add `filter.has_antitone_basis.comp_mono` and `filter.has_antitone_basis.comp_strict_mono`; * add `filter.has_antitone_basis.subbasis_with_rel`; * generalize `filter.has_basis.exists_antitone_subbasis` to `ι : Sort*`. * add a missing docstring.