id_leftLim

Mathlib.MeasureTheory.Measure.Stieltjes

URI: https://scilib.ai/kg/mathlib#StieltjesFunction.id_leftLim

← MathLib Explorer

English

The left limit of the identity Stieltjes function at x equals x.

Русский

Левый предел функции идентификатора равен x.

LaTeX

$$$$ \\text{leftLim id } x = x.$$$$

Lean4

@[simp]
theorem id_leftLim (x : ℝ) : leftLim StieltjesFunction.id x = x :=
  tendsto_nhds_unique (StieltjesFunction.id.mono.tendsto_leftLim x) <|
    continuousAt_id.tendsto.mono_left nhdsWithin_le_nhds

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru