English
Left translation by a fixed element a ∈ α preserves the uniformity: map x ↦ a·x is a uniform equivalence.
Русский
Левое перенесение на фиксированном элементе a ∈ α сохраняет униформность: отображение x ↦ a·x равно равномерно эквивалентно.
LaTeX
$$$\\bigl(\\mathcal{U}(\\alpha)\\bigr) \\text{ is invariant under } x \\mapsto a x$$$
Lean4
@[to_additive]
theorem uniformity_translate_mul (a : α) : ((𝓤 α).map fun x : α × α => (x.1 * a, x.2 * a)) = 𝓤 α :=
le_antisymm (uniformContinuous_id.mul uniformContinuous_const)
(calc
𝓤 α = ((𝓤 α).map fun x : α × α => (x.1 * a⁻¹, x.2 * a⁻¹)).map fun x : α × α => (x.1 * a, x.2 * a) := by
simp [Filter.map_map, Function.comp_def]
_ ≤ (𝓤 α).map fun x : α × α => (x.1 * a, x.2 * a) :=
Filter.map_mono (uniformContinuous_id.mul uniformContinuous_const))
