mathlib
ffde2d8a - chore(order/liminf_limsup): Generalise and move lemmas (#18628)

Commit
2 years ago
chore(order/liminf_limsup): Generalise and move lemmas (#18628) Generalise lemmas from semilattices to codirected orders. Move topology-less lemmas from `topology.algebra.order.liminf_limsup` to `order.liminf_limsup`. Also turn arguments to `bdd_above_insert` and friends implicit.
Author
Parents
Loading