smul_mem_nhds_self — Mathlib

English

If c ≠ 0, then Tendsto (x ↦ c · f(x)) l (nhds (c · a)) iff Tendsto f l (nhds a).

Русский

Если c ≠ 0, то Tendsto (x ↦ c · f(x)) l (nhds (c · a)) эквивалентно Tendsto f l (nhds a).

LaTeX

$$$\text{Tendsto}(x \mapsto c \cdot f(x))\, l\, \mathcal{N}(c \cdot a) \iff \text{Tendsto}(f)\, l\, \mathcal{N}(a)$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_mem_nhds_self [TopologicalSpace G] [ContinuousConstSMul G G] {g : G} {s : Set G} : g • s ∈ 𝓝 g ↔ s ∈ 𝓝 1 :=
  by rw [← smul_mem_nhds_smul_iff g⁻¹]; simp

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