English
The valuation map v: K → Γ₀ is a continuous function.
Русский
Оценочная отображение v: K → Γ₀ непрерывен.
LaTeX
$$$\text{Continuous}(v: K \to Γ_0)$$$
Lean4
theorem continuous_valuation [Valued K Γ₀] : Continuous (v : K → Γ₀) :=
by
rw [continuous_iff_continuousAt]
intro x
rcases eq_or_ne x 0 with (rfl | h)
· rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
intro γ hγ
rw [Filter.Eventually, Valued.mem_nhds_zero]
use Units.mk0 γ hγ; rfl
· have v_ne : (v x : Γ₀) ≠ 0 := (Valuation.ne_zero_iff _).mpr h
rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero v_ne]
apply Valued.loc_const v_ne