nhds_translation_div — Mathlib

English

In a topological group, translating by division yields a description of neighborhoods: the comap of dividing by x at 1 equals nhds at x.

Русский

В топологической группе описывается переход окрестностей через деление: отображение деления по x переводит окрестности 1 в окрестности x.

LaTeX

$$$\mathrm{nhds\_translation\_div}(x):\ comap (\lambda y. y / x) (\mathcal{N}(1)) = \mathcal{N}(x).$$$

Lean4

@[to_additive]
theorem nhds_translation_div (x : G) : comap (· / x) (𝓝 1) = 𝓝 x := by
  simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x

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