set_smul_mem_nhds_zero_iff

Mathlib.Topology.Algebra.ConstMulAction

URI: https://scilib.ai/kg/mathlib#set_smul_mem_nhds_zero_iff

← MathLib Explorer

English

For c ≠ 0, c • s ∈ nhds 0 iff s ∈ nhds 0.

Русский

Для c ≠ 0, c • s ∈ nhds 0 эквив с s ∈ nhds 0.

LaTeX

$$$c \neq 0 \Rightarrow c \cdot s \in 𝓝(0) \iff s \in 𝓝(0)$$$

Lean4

theorem set_smul_mem_nhds_zero_iff {s : Set α} {c : G₀} (hc : c ≠ 0) : c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α) :=
  by
  refine Iff.trans ?_ (smul_mem_nhds_smul_iff₀ hc)
  rw [smul_zero]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru