continuousWithinAt_Ioi_iff_rightLim_eq

English

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

Русский

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

LaTeX

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

Lean4

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

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