uniformity_eq_comap_inv_mul_nhds_one

English

The uniformity on α equals the comap of the family of neighborhoods of 1 via the map (x,y) ↦ x^{-1}y.

Русский

Униформность на α равна обратному образу по отображению (x,y) ↦ x^{-1}y от множества 𝓝(1).

LaTeX

$$$\\mathcal U(\\alpha) = \\mathrm{comap}\\bigl( (x,y) \\mapsto x^{-1}y \\bigr)\\bigl( \\mathcal N(1) \\bigr)$$$

Lean4

@[to_additive]
theorem uniformity_eq_comap_inv_mul_nhds_one : 𝓤 α = comap (fun x : α × α => x.1⁻¹ * x.2) (𝓝 (1 : α)) :=
  by
  rw [← comap_uniformity_mulOpposite, uniformity_eq_comap_nhds_one, ← op_one, ← comap_unop_nhds, comap_comap,
    comap_comap]
  simp [Function.comp_def]

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