English
A version of the Valuated topology condition: if a family of neighborhoods around 0 is generated by sets of the form { z | v(z) < γ } for units γ, then one has a valuative topology.
Русский
Версия критерия валуативной топологии: если система окрестностей вокруг 0 задаётся множест- вами { z | v(z) < γ } для единиц γ, то существует валуативная топология.
LaTeX
$$$[ContinuousConstVAdd\\ R\\ R] \\Rightarrow \\Big( \\forall s:\\ Set R,\\ s \\in 𝓝(0) \\iff \\exists γ ∈ (ValueGroupWithZero R)^{×}, \\{z\\,|\\, v(z) < γ\\} \\subseteq s \\Big) \\Rightarrow IsValuativeTopology R$$$
Lean4
/-- Assuming `ContinuousConstVAdd R R`, we only need to check the neighbourhood of `0` in order to
prove `IsValuativeTopology R`. -/
theorem of_zero [ContinuousConstVAdd R R]
(h₀ : ∀ s : Set R, s ∈ 𝓝 0 ↔ ∃ γ : (ValueGroupWithZero R)ˣ, {z | v z < γ} ⊆ s) : IsValuativeTopology R where
mem_nhds_iff
{s
x} := by simpa [← vadd_mem_nhds_vadd_iff (t := s) (-x), ← image_vadd, ← image_subset_iff] using h₀ ((x + ·) ⁻¹' s)
