smul_const for filters

Stream: Is there code for X?

[Yaël Dillies]

I'm looking for

lemma filter.tendsto.smul_const {α β M : Type*} [topological_space α] [topological_space M]
  [has_scalar M α] [has_continuous_smul M α] {f : β → M} {l : filter β}
  {c : M} (hf : filter.tendsto f l (nhds c)) (a : α) :
  filter.tendsto (λ x, (f x) • a) l (nhds (c • a)) := sorry

There's the very similar filter.tendsto.const_smul in topology.analysis.mul_action.lean, but seemingly not what I want.

[Yaël Dillies]

Bhavik points that hf.smul tendsto_const_nhds proves it.

[Bhavik Mehta]

Yaël Dillies said:

There's the very similar filter.tendsto.const_smul in topology.analysis.mul_action.lean, but seemingly not what I want.

Minor point: topology.algebra.mul_action, not analysis

[Eric Wieser]

(docs#filter.tendsto.const_smul)

[Eric Wieser]

Note that const_smul is proved as tendsto_const_nhds.smul hf

[Eric Wieser]

So the one you propose is probably just as deserving of a lemma as the one that's already there

[Bhavik Mehta]

Eric Wieser said:

Note that const_smul is proved as tendsto_const_nhds.smul hf

Right, I just looked at that and what filter.tendsto.smul said and guessed the proof of this from there!

[Benjamin Davidson]

I've seen the same thing in other places. For example we have continuous_on.const_smul but not continuous_on.smul_const; for the latter you are expected to make do with continuous_on.smul _ continuous_on_const.

[Benjamin Davidson]

(With the hypothesis about your function being continuous_on going where the _ is, or using dot-notation)