Commit 2023-09-18 15:31 ce64cd31

View on Github →

feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (#18629) Generalise bounded_le_nhds/bounded_ge_nhds using two ad hoc typeclasses. The goal here is to circumvent the fact that the product of order topologies is not an order topology, and apply those lemmas to ℝⁿ.

Estimated changes

Modified src/order/filter/pi.lean

added theorem filter.eventually.eval_pi

added theorem filter.eventually_pi

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

modified theorem Union_Ici_eq_Ioi_of_lt_of_tendsto

modified theorem Union_Iic_eq_Iio_of_lt_of_tendsto

modified theorem filter.tendsto.bdd_above_range

modified theorem filter.tendsto.bdd_above_range_of_cofinite

modified theorem filter.tendsto.bdd_below_range

modified theorem filter.tendsto.bdd_below_range_of_cofinite

modified theorem filter.tendsto.is_bounded_under_ge

modified theorem filter.tendsto.is_bounded_under_le

modified theorem filter.tendsto.is_cobounded_under_ge

modified theorem filter.tendsto.is_cobounded_under_le

modified theorem is_bounded_ge_nhds