mathlib3
d4f691b9 - feat(order/filter/basic): generalize some lemmas from `nhds_within` (#19070)

Commit

2 years ago

feat(order/filter/basic): generalize some lemmas from `nhds_within` (#19070)

Author

urkud

urkud

Parents

Loading