Theorems · Theorem · general topology

IsUnit.smul_tendsto_smul_iff

∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Monoid γ] [inst_1 : MulAction γ β] {m : α → β} {c : γ}
  {f : Filter α} {g : Filter β}, IsUnit c → (Filter.Tendsto (c • m) f (c • g) ↔ Filter.Tendsto m f g)

Defined in

Mathlib.Order.Filter.Pointwise

Cited by

2 results in Mathlib

Foundations

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

Assumes

MonoidMulAction