nhds_translation_mul_inv — Mathlib

English

If HasBasis for nhds at 1 is given, then the nhds at any x has a translated basis describing neighborhoods of x via x.

Русский

Если дана база окрестностей в точке единицы, то окрестности в любой точке x задаются посредством её переноса.

LaTeX

$$$\text{HasBasis} (\mathcal{N}_{1})\; p\; s \Rightarrow \mathcal{N}_{x} \text{ has basis } p\; (\lambda i. \{ y : y/x \in s(i) \})$$$

Lean4

@[to_additive]
theorem nhds_translation_mul_inv (x : G) : comap (· * x⁻¹) (𝓝 1) = 𝓝 x :=
  ((Homeomorph.mulRight x⁻¹).comap_nhds_eq 1).trans <| show 𝓝 (1 * x⁻¹⁻¹) = 𝓝 x by simp

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