uniformity_eq_comap_nhds_one — Mathlib

English

The uniformity on α equals the comap of the neighborhood filter at 1 under the division map x ↦ x₂/x₁.

Русский

Унииформность на α равна обратному образу фильтра окрестностей в 1 по отображению x ↦ x₂/x₁.

LaTeX

$$$\\mathcal{U}(\\alpha) = \\mathrm{comap}\\bigl(\\lambda x:(\\alpha \\times \\alpha).\\, x_2 / x_1\\bigr)(\\mathcal{N}(1))$$$

Lean4

@[to_additive]
theorem uniformity_eq_comap_nhds_one : 𝓤 α = comap (fun x : α × α => x.2 / x.1) (𝓝 (1 : α)) :=
  by
  refine eq_of_forall_le_iff fun 𝓕 ↦ ?_
  rw [nhds_eq_comap_uniformity, comap_comap, ← tendsto_iff_comap, ←
    (tendsto_diag_uniformity Prod.fst 𝓕).uniformity_mul_iff_left, ← tendsto_id']
  congrm Tendsto ?_ _ _
  ext <;> simp

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