English
For every γ ∈ Γ₀ˣ, closure of { x ∈ K | v(x) < γ } equals { x ∈ hat K | extensionValuation(x) < γ }.
Русский
Для каждого γ ∈ Γ₀ˣ замыкание множества { x ∈ K | v(x) < γ } в hat K равно { x ∈ hat K | extensionValuation(x) < γ }.
LaTeX
$$$\forall γ \in Γ_0^{\times},\; closure( { x \in K \mid v(x) < γ } ) = { x \in \hat{K} \mid extensionValuation(x) < γ }$$$
Lean4
theorem closure_coe_completion_v_lt {γ : Γ₀ˣ} :
closure ((↑) '' {x : K | v x < (γ : Γ₀)}) = {x : hat K | extensionValuation x < (γ : Γ₀)} :=
by
ext x
let γ₀ := extensionValuation x
suffices γ₀ ≠ 0 → (x ∈ closure ((↑) '' {x : K | v x < (γ : Γ₀)}) ↔ γ₀ < (γ : Γ₀))
by
rcases eq_or_ne γ₀ 0 with h | h
· simp only [(Valuation.zero_iff _).mp h, mem_setOf_eq, Valuation.map_zero, Units.zero_lt, iff_true]
apply subset_closure
exact ⟨0, by simp only [mem_setOf_eq, Valuation.map_zero, Units.zero_lt, true_and]; rfl⟩
· exact this h
intro h
have hγ₀ : extension ⁻¹' { γ₀ } ∈ 𝓝 x :=
continuous_extension.continuousAt.preimage_mem_nhds (WithZeroTopology.singleton_mem_nhds_of_ne_zero h)
rw [mem_closure_iff_nhds']
refine ⟨fun hx => ?_, fun hx s hs => ?_⟩
· obtain ⟨⟨-, y, hy₁ : v y < (γ : Γ₀), rfl⟩, hy₂⟩ := hx _ hγ₀
replace hy₂ : v y = γ₀ := by simpa using hy₂
rwa [← hy₂]
· obtain ⟨y, hy₁, hy₂⟩ := Completion.denseRange_coe.mem_nhds (inter_mem hγ₀ hs)
replace hy₁ : v y = γ₀ := by simpa using hy₁
rw [← hy₁] at hx
exact ⟨⟨y, ⟨y, hx, rfl⟩⟩, hy₂⟩
