Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-08-28 11:58 ffde2d8a

View on Github →

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.

Estimated changes

deleted theorem bdd_above.insert
modified theorem bdd_above.union
modified theorem bdd_above_insert
modified theorem bdd_above_union
modified theorem bdd_below.insert
modified theorem bdd_below.union
modified theorem bdd_below_insert
modified theorem bdd_below_union
added def scott_continuous