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
.