English
Let α be a linearly ordered commutative group endowed with an order topology. For every a ∈ α, the neighborhood filter 𝓝(a) is the infimum of the principal filters of the sets { b ∈ α : |a / b|_m < r } taken over all r > 1.
Русский
Пусть α - линейно упорядоченная коммутативная группа с порядковой топологией. Для каждого a ∈ α окрестностный фильтр 𝓝(a) равен инфимума над r > 1 от лидирующих фильтров множества { b ∈ α : |a / b|_m < r }.
LaTeX
$$$$\mathcal{N}(a) = \inf_{r>1} \mathcal{P}\{ b \in \alpha : |a/b|_{m} < r \}$$$$
Lean4
@[to_additive]
theorem nhds_eq_iInf_mabs_div (a : α) : 𝓝 a = ⨅ r > 1, 𝓟 {b | |a / b|ₘ < r} :=
by
simp only [nhds_eq_order, mabs_lt, setOf_and, ← inf_principal, iInf_inf_eq]
refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)
· refine (Equiv.divLeft a).iInf_congr fun x => ?_; simp [Ioi]
· refine (Equiv.divRight a).iInf_congr fun x => ?_; simp [Iio]
