Theorems · Theorem · general topology

tendsto_const_smul_iff

∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {f : β → α} {l : Filter β} {a : α} (c : G),
  Filter.Tendsto (fun x => c • f x) l (nhds (c • a)) ↔ Filter.Tendsto f l (nhds a)

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

5 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceGroupMulActionContinuousConstSMul