Commit 2023-01-31 22:01 5098b9fc

View on Github →

feat: port Topology.Algebra.Order.LeftRight (#1931)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Order/LeftRight.lean

added theorem continuousAt_iff_continuous_left'_right'

added theorem continuousAt_iff_continuous_left_right

added theorem continuousWithinAt_Iio_iff_Iic

added theorem continuousWithinAt_Ioi_iff_Ici

added theorem nhds_left'_le_nhds_ne

added theorem nhds_left'_sup_nhds_right'

added theorem nhds_left'_sup_nhds_right

added theorem nhds_left_sup_nhds_right'

added theorem nhds_left_sup_nhds_right

added theorem nhds_right'_le_nhds_ne