singleton_mul_mem_nhds_of_nhds_one

English

If nhds of b contains s, then nhds of ab contains a·s, i.e., s·{a} is neighborhood of ab whenever s is neighborhood of b.

Русский

Если s ⊆ nhds(b), то s·{a} ⊆ nhds(a·b); т.е. {a}·s является окрестностью a·b.

LaTeX

$$$\\{a\\}\\cdot s \\in \\mathcal N(a\\cdot b) \\quad\\text{whenever } s\\in \\mathcal N(b).$$$

Lean4

@[to_additive]
theorem singleton_mul_mem_nhds_of_nhds_one (a : α) (h : s ∈ 𝓝 (1 : α)) : { a } * s ∈ 𝓝 a := by
  simpa only [mul_one] using singleton_mul_mem_nhds a h

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