leftLim — Mathlib

English

A monotone f is left continuous at x if and only if leftLim f x = f x when restricting to left side Iio x.

Русский

Для монотонной f лево-непрерывность в точке x эквивалентна равенству leftLim f x = f x при ограничении слева Iio x.

LaTeX

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

Lean4

@[mono]
protected theorem leftLim : Monotone (leftLim f) := by
  intro x y h
  rcases eq_or_lt_of_le h with (rfl | hxy)
  · exact le_rfl
  · exact (hf.leftLim_le le_rfl).trans (hf.le_leftLim hxy)

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