Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 18:21 a779f6cf

View on Github →

feat(topology/algebra/ordered): convergent sequence is bounded above/below (#10424) Also move lemmas Ixx_mem_nhds up to generalize them from [linear_order α] [order_topology α] to [linear_order α] [order_closed_topology α].

Estimated changes

Modified src/order/liminf_limsup.lean

added theorem filter.is_bounded_under.bdd_above_range

added theorem filter.is_bounded_under.bdd_above_range_of_cofinite

added theorem filter.is_bounded_under.bdd_below_range

added theorem filter.is_bounded_under.bdd_below_range_of_cofinite

modified theorem filter.not_is_bounded_under_of_tendsto_at_bot

modified theorem filter.not_is_bounded_under_of_tendsto_at_top

Modified src/topology/algebra/ordered/basic.lean

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

added theorem filter.tendsto.bdd_above_range

added theorem filter.tendsto.bdd_above_range_of_cofinite

added theorem filter.tendsto.bdd_below_range

added theorem filter.tendsto.bdd_below_range_of_cofinite