countable_leftLim_ne — Mathlib

English

The set { x | leftLim f x ≠ f x } is countable for a fixed Stieltjes function f.

Русский

Множество {x | leftLim f x ≠ f x} счетно.

LaTeX

$$$$ \\{x \\mid \\text{leftLim } f x \\neq f x\\} \\text{ is countable}. $$$$

Lean4

theorem countable_leftLim_ne (f : StieltjesFunction) : Set.Countable {x | leftLim f x ≠ f x} :=
  by
  refine Countable.mono ?_ f.mono.countable_not_continuousAt
  intro x hx h'x
  apply hx
  exact tendsto_nhds_unique (f.mono.tendsto_leftLim x) (h'x.tendsto.mono_left nhdsWithin_le_nhds)

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