English
For NoMaxOrder α, the neighborhood 𝓝(a) has a basis given by Ioo(a/ε, a·ε) with ε > 1.
Русский
Для NoMaxOrder α окрестности 𝓝(a) имеют базис вида Ioo(a/ε, a·ε) при ε>1.
LaTeX
$$$$ (\mathcal{N}(a)).HasBasis (\lambda \varepsilon: \alpha. (1<\varepsilon)) (\lambda \varepsilon. Ioo\left(a/\varepsilon, a\cdot\varepsilon\right)). $$$$
Lean4
@[to_additive]
theorem nhds_basis_Ioo_one_lt [NoMaxOrder α] (a : α) :
(𝓝 a).HasBasis (fun ε : α => (1 : α) < ε) fun ε => Ioo (a / ε) (a * ε) :=
by
convert nhds_basis_mabs_div_lt a
simp only [Ioo, mabs_lt, ← div_lt_iff_lt_mul, inv_lt_div_iff_lt_mul, div_lt_comm]