English
An is strict ordered ring 𝕜 with a norm-based basis of neighborhoods at 0 yields a topological ring structure via a continuous inverse at 0.
Русский
Для строгой упорядоченной кольцевой структуры с нормой, задающей окрестности нуля, существует топологическая структура кольца с непрерывным обратным рядом около нуля.
LaTeX
$$$\text{IsTopologicalRing}(\mathbb{K})$ follows from a norm-based basis of neighborhoods at 0.$$
Lean4
/-- If a (possibly non-unital and/or non-associative) ring `R` admits a submultiplicative
nonnegative norm `norm : R → 𝕜`, where `𝕜` is a linear ordered field, and the open balls
`{ x | norm x < ε }`, `ε > 0`, form a basis of neighborhoods of zero, then `R` is a topological
ring. -/
theorem of_norm {R 𝕜 : Type*} [NonUnitalNonAssocRing R] [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
[TopologicalSpace R] [IsTopologicalAddGroup R] (norm : R → 𝕜) (norm_nonneg : ∀ x, 0 ≤ norm x)
(norm_mul_le : ∀ x y, norm (x * y) ≤ norm x * norm y)
(nhds_basis : (𝓝 (0 : R)).HasBasis ((0 : 𝕜) < ·) (fun ε ↦ {x | norm x < ε})) : IsTopologicalRing R :=
by
have h0 : ∀ f : R → R, ∀ c ≥ (0 : 𝕜), (∀ x, norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0) :=
by
refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩
refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩
exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ
apply IsTopologicalRing.of_addGroup_of_nhds_zero
case hmul =>
refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
simp only at *
calc
norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
_ < ε := (mul_le_of_le_one_left (norm_nonneg _) hx.le).trans_lt hy
case hmul_left => exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)
case hmul_right =>
exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x => (norm_mul_le x y).trans_eq (mul_comm _ _)
