continuousWithinAt_Iio_iff_leftLim_eq

English

An antitone function is continuous to the left at a point x if and only if the left limit equals the value: ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x.

Русский

Антимонотонная функция непрерывна слева в точке x тогда и только тогда, когда левый предел равен значению: ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x.

LaTeX

$$$\text{Antitone}(f) \Rightarrow (\text{ContinuousWithinAt}(f,\mathrm{Iio}(x),x) \iff \operatorname{leftLim} f x = f x)$$$

Lean4

/-- An antitone function is continuous to the left at a point if and only if its left limit
coincides with the value of the function. -/
theorem continuousWithinAt_Iio_iff_leftLim_eq : ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x :=
  hf.dual_right.continuousWithinAt_Iio_iff_leftLim_eq

Похожие утверждения