discreteTopology_of_forall_map_eq_one

English

There exists an instance IsTopologicalRing making the ring R a topological ring under valuation-induced topology.

Русский

Существует структура IsTopologicalRing, делающая кольцо R топологическим кольцом с топологией, задаваемой оценкой.

LaTeX

$$$IsTopologicalRing(R)$$$

Lean4

theorem discreteTopology_of_forall_map_eq_one (h : ∀ x : R, x ≠ 0 → v x = 1) : DiscreteTopology R :=
  by
  simp only [discreteTopology_iff_isOpen_singleton_zero, isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq,
    mem_nhds_zero, subset_singleton_iff, mem_setOf_eq]
  use 1
  contrapose! h
  obtain ⟨x, hx, hx'⟩ := h
  exact ⟨x, hx', hx.ne⟩

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