uniformity_basis_edist_inv_two_pow

English

The uniformity on α has a basis given by sets { (x,y) : edist(x,y) < 2^{-1}^n } for n ∈ ℕ.

Русский

Униформность на α имеет базис { (x,y) : edist(x,y) < 2^{-1}^n } для натуральных n.

LaTeX

$$$ (\mathcal{U}_\alpha) \text{ has basis } \{V_n\}_{n\in\mathbb{N}},\quad V_n = \{(x,y) \in \alpha \times \alpha : \operatorname{edist}(x,y) < 2^{-1}^{n}\}. $$$

Lean4

theorem uniformity_basis_edist_inv_two_pow :
    (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => {p : α × α | edist p.1 p.2 < 2⁻¹ ^ n} :=
  EMetric.mk_uniformity_basis (fun _ _ ↦ ENNReal.pow_pos (ENNReal.inv_pos.2 ENNReal.ofNat_ne_top) _) fun _ε ε₀ ↦
    let ⟨n, hn⟩ := ENNReal.exists_inv_two_pow_lt (ne_of_gt ε₀)
    ⟨n, trivial, le_of_lt hn⟩

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