tendsto_const_smul_iff₀ — Mathlib

English

For a nonzero topological group, g ∈ G and s ⊆ G, g · s ∈ nhds(g) iff s ∈ nhds(1).

Русский

Для группы с нулём, g ∈ G и s ⊆ G, g · s ∈ nhds(g) тогда и только тогда, когда s ∈ nhds(1).

LaTeX

$$$g \cdot s \in \mathcal{N}(g) \iff s \in \mathcal{N}(1)$$$

Lean4

theorem tendsto_const_smul_iff₀ {f : β → α} {l : Filter β} {a : α} {c : G₀} (hc : c ≠ 0) :
    Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
  tendsto_const_smul_iff (Units.mk0 c hc)

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