nhds_basis_Icc_one_lt — Mathlib

English

Under NoMaxOrder and densely ordered α, the neighborhood basis around a is given by Icc(a/ε, a·ε) with ε > 1.

Русский

При NoMaxOrder и плотно упорядоченном α базис окрестностей 𝓝(a) задан через Icc(a/ε, a·ε) при ε>1.

LaTeX

$$$$ (\mathcal{N}(a)).HasBasis (\lambda \varepsilon: \alpha. (1<\varepsilon)) (\lambda \varepsilon. Icc(a/\varepsilon, a\cdot\varepsilon)). $$$$

Lean4

@[to_additive]
theorem nhds_basis_Icc_one_lt [NoMaxOrder α] [DenselyOrdered α] (a : α) :
    (𝓝 a).HasBasis ((1 : α) < ·) fun ε ↦ Icc (a / ε) (a * ε) :=
  (nhds_basis_Ioo_one_lt a).to_hasBasis
    (fun _ε ε₁ ↦
      let ⟨δ, δ₁, δε⟩ := exists_between ε₁
      ⟨δ, δ₁, Icc_subset_Ioo (by gcongr) (by gcongr)⟩)
    (fun ε ε₁ ↦ ⟨ε, ε₁, Ioo_subset_Icc_self⟩)

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