discreteTopology_of_forall_lt — Mathlib

English

Under suitable hypotheses, the valued field K carries the discrete topology.

Русский

При соответствующих гипотезах у valued-поле K дискретная топология.

LaTeX

$$$DiscreteTopology(K)$$$

Lean4

theorem discreteTopology_of_forall_lt [MulArchimedean Γ₀] [Valued K Γ₀] {r : Γ₀} (hr : r ≠ 0)
    (h : ∀ x : K, v x ≠ 0 → r < v x) : DiscreteTopology K :=
  discreteTopology_of_forall_map_eq_one (by simpa using Valued.v.map_eq_one_of_forall_lt hr h)

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