nhds_basis_Ioo_one_lt — Mathlib

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]

Похожие утверждения