mem_nhds_iff' — Mathlib

English

For IsValuativeTopology R, the lemma mem_nhds_iff' expresses nhds neighborhoods via shifts: s ∈ 𝓝 x iff ∃ γ, { z | v(z − x) < γ } ⊆ s.

Русский

Для IsValuativeTopology R лемма mem_nhds_iff' выражает окрестности 𝓝 x через сдвиги: s ∈ 𝓝 x тогда и только тогда, когда существует γ, такое что { z | v(z − x) < γ } ⊆ s.

LaTeX

$$$\\forall x,\\ s \\in 𝓝(x) \\iff \\exists γ \\in (ValueGroupWithZero R)^{×},\\ {z \\mid v(z - x) < γ} \\subseteq s$$$

Lean4

/-- A version mentioning subtraction. -/
theorem mem_nhds_iff' {s : Set R} {x : R} : s ∈ 𝓝 (x : R) ↔ ∃ γ : (ValueGroupWithZero R)ˣ, {z | v (z - x) < γ} ⊆ s :=
  by
  convert mem_nhds_iff (s := s) using 4
  ext z
  simp [neg_add_eq_sub]

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