continuous_valuation — Mathlib

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

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