tendsto_of_ne_zero — Mathlib

English

A set s is open in the zero-adjoined topology iff either 0 ∉ s or there exists a nonzero γ with Iio(γ) ⊆ s.

Русский

Множество s открыто в топологии, сопоставляемой нулю, тогда и только тогда, если 0 ∉ s или существует γ ≠ 0 с Iio(γ) ⊆ s.

LaTeX

$$$\text{IsOpen}(s) \iff (0 \in s)^c \ \/\ \exists \gamma ≠ 0, Iio(\gamma) \subseteq s$$$

Lean4

theorem tendsto_of_ne_zero {γ : Γ₀} (h : γ ≠ 0) : Tendsto f l (𝓝 γ) ↔ ∀ᶠ x in l, f x = γ := by
  rw [nhds_of_ne_zero h, tendsto_pure]

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