leftLim_eq_of_eq_bot — Mathlib

English

If nhds[<] a = ⊥, then leftLim f a = f a.

Русский

Если левая окрестность nhds[<] a тождественно пустая, то левая граница равна значению в точке: leftLim f a = f a.

LaTeX

$$$\nhds[<] a = ⊥ \Rightarrow \operatorname{leftLim}(f,a) = f(a)$$$

Lean4

theorem leftLim_eq_of_eq_bot [hα : TopologicalSpace α] [h'α : OrderTopology α] (f : α → β) {a : α} (h : 𝓝[<] a = ⊥) :
    leftLim f a = f a := by
  rw [h'α.topology_eq_generate_intervals] at h
  simp [leftLim, h]

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