English
For NoMaxOrder α, the neighborhood 𝓃𝒹𝓈(a) has a basis consisting of sets { b : |b / a|_m < ε } with ε > 1.
Русский
Для NoMaxOrder α окрестности 𝓝(a) обладают базисом вида { b : |b/a|_m < ε } при ε>1.
LaTeX
$$$$ (\mathcal{N}(a)).HasBasis (\lambda \varepsilon:\alpha. 1<\varepsilon) (\lambda \varepsilon. \{ b \in \alpha : |b/a|_{m} < \varepsilon \}). $$$$
Lean4
@[to_additive]
theorem nhds_basis_mabs_div_lt [NoMaxOrder α] (a : α) :
(𝓝 a).HasBasis (fun ε : α => (1 : α) < ε) fun ε => {b | |b / a|ₘ < ε} :=
by
simp only [nhds_eq_iInf_mabs_div, mabs_div_comm (a := a)]
refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)
exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _), fun _ hz => hz.trans_le (min_le_right _ _)⟩
