mathlib
4faf2e21 - chore(order/filter): use implicit arguments in `tendsto_at_top` etc (#4672)

Commit

5 years ago

chore(order/filter): use implicit arguments in `tendsto_at_top` etc (#4672) Also weaken some assumptions from a decidable linear order to a linear order.

References

#4925 - Make prime-avoidance branch build

Author

urkud

Parents

392d52c2

mathlib 4faf2e21 - chore(order/filter): use implicit arguments in `tendsto_at_top` etc (#4672)

mathlib
4faf2e21 - chore(order/filter): use implicit arguments in `tendsto_at_top` etc (#4672)