English
The structure R carries a topology making ring operations continuous, i.e., R is a topological ring.
Русский
Структура R оснащена топологией, делающей непрерывными операции умножения и сложения, то есть R — топологическое кольцо.
LaTeX
$$IsTopologicalRing R$$
Lean4
instance (priority := low) isTopologicalAddGroup : IsTopologicalAddGroup R :=
by
have cts_add : ContinuousConstVAdd R R :=
⟨fun x ↦
continuous_iff_continuousAt.2 fun z ↦
((hasBasis_nhds z).tendsto_iff (hasBasis_nhds (x + z))).2 fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩⟩
have basis := hasBasis_nhds_zero R
refine .of_comm_of_nhds_zero ?_ ?_ fun x₀ ↦ (map_eq_of_inverse (-x₀ + ·) ?_ ?_ ?_).symm
· exact (basis.prod_self.tendsto_iff basis).2 fun γ _ ↦ ⟨γ, trivial, fun ⟨_, _⟩ hx ↦ (v).map_add_lt hx.left hx.right⟩
· exact (basis.tendsto_iff basis).2 fun γ _ ↦ ⟨γ, trivial, fun y hy ↦ by simpa using hy⟩
· ext; simp
· simpa [ContinuousAt] using (cts_add.1 x₀).continuousAt (x := (0 : R))
· simpa [ContinuousAt] using (cts_add.1 (-x₀)).continuousAt (x := x₀)
