mul_singleton_mem_nhds — Mathlib

English

For any a ∈ α and any neighborhood h of b, the product s·{a} is a neighborhood of ab whenever s is a neighborhood of b.

Русский

Для любого a и окрестности h в b, произведение s·{a} является окрестностью ab, если s — окрестность b.

LaTeX

$$$\\text{mul\_singleton\_mem\_nhds}(a; b; h): s\\cdot\\{a\\} \\in \\mathcal N(a\\cdot b).$$$

Lean4

@[to_additive]
theorem mul_singleton_mem_nhds (a : α) {b : α} (h : s ∈ 𝓝 b) : s * { a } ∈ 𝓝 (b * a) :=
  by
  rw [mul_singleton]
  exact smul_mem_nhds_smul (op a) h

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