Commit 2023-02-13 22:40 a4371c91

View on Github →

feat: port Topology.Algebra.Order.LeftRightLim (#2131)

Estimated changes

Modified Mathlib.lean

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

added theorem Antitone.continuousAt_iff_leftLim_eq_rightLim

added theorem Antitone.continuousWithinAt_Iio_iff_leftLim_eq

added theorem Antitone.continuousWithinAt_Ioi_iff_rightLim_eq

added theorem Antitone.countable_not_continuousAt

added theorem Antitone.le_leftLim

added theorem Antitone.le_rightLim

added theorem Antitone.leftLim_le

added theorem Antitone.leftLim_le_rightLim

added theorem Antitone.rightLim_le

added theorem Antitone.rightLim_le_leftLim

added theorem Antitone.tendsto_leftLim

added theorem Antitone.tendsto_leftLim_within

added theorem Antitone.tendsto_rightLim

added theorem Antitone.tendsto_rightLim_within

added theorem Monotone.continuousAt_iff_leftLim_eq_rightLim

added theorem Monotone.continuousWithinAt_Iio_iff_leftLim_eq

added theorem Monotone.continuousWithinAt_Ioi_iff_rightLim_eq

added theorem Monotone.countable_not_continuousAt

added theorem Monotone.countable_not_continuousWithinAt_Iio

added theorem Monotone.countable_not_continuousWithinAt_Ioi

added theorem Monotone.le_leftLim

added theorem Monotone.le_rightLim

added theorem Monotone.leftLim_eq_supₛ

added theorem Monotone.leftLim_le

added theorem Monotone.leftLim_le_rightLim

added theorem Monotone.rightLim_le

added theorem Monotone.rightLim_le_leftLim

added theorem Monotone.tendsto_leftLim

added theorem Monotone.tendsto_leftLim_within

added theorem Monotone.tendsto_rightLim

added theorem Monotone.tendsto_rightLim_within

added theorem leftLim_eq_of_eq_bot

added theorem leftLim_eq_of_tendsto