nhds_of_one — Mathlib

English

If nhds(1) has a HasBasis with index ι, p, s, then nhds(x) has HasBasis with p and sets { y | y/x ∈ s i }.

Русский

Если у окрестностей единицы есть база HasBasis, то окрестности 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_of_one {ι : Sort*} {p : ι → Prop} {s : ι → Set G} (hb : HasBasis (𝓝 1 : Filter G) p s) (x : G) :
    HasBasis (𝓝 x) p fun i => {y | y / x ∈ s i} :=
  by
  rw [← nhds_translation_mul_inv]
  simp_rw [div_eq_mul_inv]
  exact hb.comap _

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