English
If an additive group (with the order topology) satisfies that for every a the neighborhood 𝓝(a) equals the infimum over r>1 of principal filters of { b : |a / b|_m < r }, then the given structure supports the order topology.
Русский
Если для каждой точки a в группе с порядком окрестности удовлетворяют равенству 𝓝(a) = ∑ inf_{r>1} 𝓟{ b : |a/b|_m < r }, тогда на множестве определяется порядоковая топология.
LaTeX
$$$$\forall a\in\alpha:\quad \mathcal{N}(a) = \inf_{r>1} \mathcal{P}\{ b\in\alpha : |a/b|_{m} < r \} \implies \text{OrderTopology } \alpha.$$$$
Lean4
@[to_additive]
theorem orderTopology_of_nhds_mabs {α : Type*} [TopologicalSpace α] [CommGroup α] [LinearOrder α] [IsOrderedMonoid α]
(h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 1, 𝓟 {b | |a / b|ₘ < r}) : OrderTopology α :=
by
refine ⟨TopologicalSpace.ext_nhds fun a => ?_⟩
rw [h_nhds]
letI := Preorder.topology α; letI : OrderTopology α := ⟨rfl⟩
exact (nhds_eq_iInf_mabs_div a).symm
