Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-07 06:39 ba1cbfac

View on Github →

feat(topology/algebra/ordered/basic): Add alternative formulations of four lemmas. (#10630) Add alternative formulations of lemmas about interiors and frontiers of Iic and Ici. The existing formulations make typeclass assumptions [no_top_order] or [no_bot_order]. These alternative formulations assume instead that the endpoint of the interval is not top or bottom; and as such they can be applied in, e.g., nnreal and ennreal. Also, some lemmas now assume (Ioi a).nonempty or (Iio a).nonempty instead of {b} (h : a < b) or {b} (h : b < a), respectively.

Estimated changes

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

modified theorem closure_Iio'

modified theorem closure_Ioi'

added theorem frontier_Ici'

modified theorem frontier_Ici

added theorem frontier_Iic'

modified theorem frontier_Iic

added theorem frontier_Iio'

modified theorem frontier_Iio

added theorem frontier_Ioi'

modified theorem frontier_Ioi

added theorem interior_Ici'

modified theorem interior_Ici

added theorem interior_Iic'

modified theorem interior_Iic

modified theorem nhds_within_Iio_ne_bot'

modified theorem nhds_within_Iio_self_ne_bot'

modified theorem nhds_within_Ioi_ne_bot'

modified theorem nhds_within_Ioi_self_ne_bot'

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

Modified src/topology/instances/ennreal.lean