nhds_basis_one_mabs_lt — Mathlib

English

The neighborhood basis at 1 is given by { b : |b|_m < ε } with ε > 1, for NoMaxOrder α.

Русский

Базис окрестностей в точке 1 задаётся как { b : |b|_m < ε } при ε > 1.

LaTeX

$$$$ (\mathcal{N}(1)).HasBasis (\lambda \varepsilon. 1<\varepsilon) (\lambda \varepsilon. \{ b : |b|_{m} < \varepsilon \}). $$$$

Lean4

@[to_additive]
theorem nhds_basis_one_mabs_lt [NoMaxOrder α] :
    (𝓝 (1 : α)).HasBasis (fun ε : α => (1 : α) < ε) fun ε => {b | |b|ₘ < ε} := by
  simpa using nhds_basis_mabs_div_lt (1 : α)

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