uniformity_eq_comap_inv_mul_nhds_one_swapped

English

A symmetry holds: the uniformity on α can also be described using the swapped map (x,y) ↦ y^{-1}x.

Русский

Сохранение симметрии: униформность на α может быть описана через отображение (x,y) ↦ y^{-1}x.

LaTeX

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

Lean4

@[to_additive]
theorem uniformity_eq_comap_inv_mul_nhds_one_swapped : 𝓤 α = comap (fun x : α × α => x.2⁻¹ * x.1) (𝓝 (1 : α)) :=
  by
  rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap]
  rfl

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