mem_nhds_zero — Mathlib

English

The nhds description around x is equivalent to the existence of a γ- neighborhood: x ∈ nhds(y) described by valuations.

Русский

Описание окрестности вокруг x эквивалентно существованию окрестности по γ через оценки.

LaTeX

$$$s \in nhds(x) \iff \exists \gamma, {y: R : v(y-x) < \gamma} \subseteq s$$$

Lean4

theorem mem_nhds_zero {s : Set R} : s ∈ 𝓝 (0 : R) ↔ ∃ γ : Γ₀ˣ, {x | v x < (γ : Γ₀)} ⊆ s := by
  simp only [mem_nhds, sub_zero]

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