separated — Mathlib

English

A valued division ring is a separated (T0) space.

Русский

Ценностное деление кольцо является разделимым пространством (T0).

LaTeX

$$$T_0Space(K)$$$

Lean4

/-- A valued division ring is separated. -/
instance (priority := 100) separated [Valued K Γ₀] : T0Space K :=
  by
  suffices T2Space K by infer_instance
  apply IsTopologicalAddGroup.t2Space_of_zero_sep
  intro x x_ne
  refine ⟨{k | v k < v x}, ?_, fun h => lt_irrefl _ h⟩
  rw [Valued.mem_nhds]
  have vx_ne := (Valuation.ne_zero_iff <| v).mpr x_ne
  let γ' := Units.mk0 _ vx_ne
  exact ⟨γ', fun y hy => by simpa using hy⟩

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