mem_nhds — Mathlib

English

Characterization of membership in nhds(x): s ∈ nhds(x) iff ∃ γ ∈ Γ₀ˣ with { y ∈ R : v(y − x) < γ } ⊆ s.

Русский

Участие множества s в окрестностях nhds(x): ∃ γ ∈ Γ₀ˣ такое, что { y : R | v(y − x) < γ } ⊆ s.

LaTeX

$$$s \in \mathcal{N}(x) \iff \exists \gamma \in Γ_0^{\times}, \{y\in R : v(y-x) < \gamma\} \subseteq s$$$

Lean4

theorem mem_nhds {s : Set R} {x : R} : s ∈ 𝓝 x ↔ ∃ γ : Γ₀ˣ, {y | (v (y - x) : Γ₀) < γ} ⊆ s := by
  simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_setOf_eq, true_and,
    ((hasBasis_nhds_zero R Γ₀).comap fun y => y - x).mem_iff]

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