Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 09:10 c294e4bb

View on Github →

feat(topology/*): replace some a < b assumptions with a ≠ b (#11650)

Estimated changes

Modified src/analysis/box_integral/box/basic.lean

added theorem box_integral.box.lower_ne_upper

Modified src/analysis/calculus/extend_deriv.lean

Modified src/analysis/calculus/local_extr.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/special_functions/trigonometric/basic.lean

Modified src/measure_theory/integral/interval_integral.lean

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

modified theorem closure_Ico

modified theorem closure_Ioc

modified theorem closure_Ioo

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