limUnder_of_not_tendsto — Mathlib

English

If there is no x with Tendsto g f (nhds x), then limUnder f g equals a fixed chosen element of X.

Русский

Если не существует x such that Tendsto g f (nhds x), то limUnder f g равно фиксированному элементу X.

LaTeX

$$$\neg \exists x, \operatorname{Tendsto} g f (\nhds x) \Rightarrow \operatorname{limUnder} f g = \operatorname{Classical.choice} \; hX$$$

Lean4

theorem limUnder_of_not_tendsto [hX : Nonempty X] {f : Filter α} {g : α → X} (h : ¬∃ x, Tendsto g f (𝓝 x)) :
    limUnder f g = Classical.choice hX := by
  simp_rw [Tendsto] at h
  simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]

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