smul_mem_nhds_smul_iff₀ — Mathlib

English

For a nonzero element c (unit), c • s ∈ nhds (c • a) is equivalent to s ∈ nhds a.

Русский

Для ненулевого элемента c: c • s ∈ nhds(c • a) эквивалентно s ∈ nhds a.

LaTeX

$$$c \cdot s \in 𝓝 (c \cdot a) \iff s \in 𝓝 a$$$

Lean4

/-- Scalar multiplication by a nonzero scalar preserves neighborhoods. -/
theorem smul_mem_nhds_smul_iff₀ {c : G₀} {s : Set α} {x : α} (hc : c ≠ 0) : c • s ∈ 𝓝 (c • x : α) ↔ s ∈ 𝓝 x :=
  smul_mem_nhds_smul_iff (Units.mk0 c hc)

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