English
Two uniform structures that arise fromIsUniformGroup coincide with the given uniform space: IsUniformGroup.toUniformSpace equals the ambient UniformSpace.
Русский
Две структуры униформности, возникающие из IsUniformGroup, совпадают с заданной uniforme пространством: IsUniformGroup.toUniformSpace = заданное.
LaTeX
$$$IsUniformGroup.toUniformSpace(G) = u$$$
Lean4
/-- The right uniformity on a topological group (as opposed to the left uniformity).
Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformGroup` structure. Two important special cases where they _do_ coincide are for
commutative groups (see `isUniformGroup_of_commGroup`) and for compact groups (see
`IsUniformGroup.of_compactSpace`). -/
@[to_additive /-- The right uniformity on a topological additive group (as opposed to the left
uniformity).
Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformAddGroup` structure. Two important special cases where they _do_ coincide are for
commutative additive groups (see `isUniformAddGroup_of_addCommGroup`) and for compact
additive groups (see `IsUniformAddGroup.of_compactSpace`). -/
]
def toUniformSpace : UniformSpace G
where
uniformity := comap (fun p : G × G => p.2 / p.1) (𝓝 1)
symm :=
have : Tendsto (fun p : G × G ↦ (p.2 / p.1)⁻¹) (comap (fun p : G × G ↦ p.2 / p.1) (𝓝 1)) (𝓝 1⁻¹) :=
tendsto_id.inv.comp tendsto_comap
by simpa [tendsto_comap_iff]
comp :=
Tendsto.le_comap fun U H ↦ by
rcases exists_nhds_one_split H with ⟨V, V_nhds, V_mul⟩
refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)
rintro ⟨x, y⟩ ⟨z, hz₁, hz₂⟩
simpa using V_mul _ hz₂ _ hz₁
nhds_eq_comap_uniformity _ := by simp only [comap_comap, Function.comp_def, nhds_translation_div]
