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

Modified src/data/set/finite.lean

modified theorem set.infinite_of_not_bdd_below

Modified src/order/bounds/basic.lean

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

Modified src/order/directed.lean

deleted def scott_continuous

Modified src/order/liminf_limsup.lean

added theorem filter.bdd_above_range_of_tendsto_at_top_at_bot

added theorem filter.bdd_below_range_of_tendsto_at_top_at_top

added theorem filter.gt_mem_sets_of_Liminf_gt

added theorem filter.is_bounded_ge_at_top

added theorem filter.is_bounded_le_at_bot

modified theorem filter.is_bounded_under.bdd_above_range

modified theorem filter.is_bounded_under.bdd_above_range_of_cofinite

modified theorem filter.is_bounded_under.bdd_below_range

modified theorem filter.is_bounded_under.bdd_below_range_of_cofinite

added theorem filter.lt_mem_sets_of_Limsup_lt

added theorem filter.tendsto.is_bounded_under_ge_at_top

added theorem filter.tendsto.is_bounded_under_le_at_bot

Modified src/topology/algebra/order/liminf_limsup.lean

deleted theorem bdd_above_range_of_tendsto_at_top_at_bot

deleted theorem bdd_below_range_of_tendsto_at_top_at_top

deleted theorem filter.tendsto.is_bounded_under_ge_at_top

deleted theorem filter.tendsto.is_bounded_under_le_at_bot

deleted theorem gt_mem_sets_of_Liminf_gt

deleted theorem is_bounded_ge_at_top

deleted theorem is_bounded_le_at_bot

deleted theorem lt_mem_sets_of_Limsup_lt