mul_self — Mathlib

English

If the neighborhood filter at 1 has a basis given by p and s, then it also has a basis given by p and the sets s i · s i.

Русский

Если у фильтра окрестностей в точке 1 есть база вида p и s, то фильтр окрестностей в 1 имеет базу p и s i·s i.

LaTeX

$$$((nhds 1).HasBasis\ p\ s) \Rightarrow (nhds 1).HasBasis\ p\ (\lambda i, s i \cdot s i)$$$

Lean4

@[to_additive]
theorem mul_self {p : ι → Prop} {s : ι → Set M} (h : (𝓝 1).HasBasis p s) : (𝓝 1).HasBasis p fun i => s i * s i :=
  by
  rw [← nhds_mul_nhds_one, ← map₂_mul, ← map_uncurry_prod]
  simpa only [← image_mul_prod] using h.prod_self.map _

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