Tendsto.filter_mono

Stream: Is there code for X?

[Vincent Beffara]

Is there a name for this?

example {f : ℝ → ℝ} {p₁ p₂ : Filter ℝ} (h : p₁ ≤ p₂) (hf : Tendsto f p₂ (𝓝 0)) : Tendsto f p₁ (𝓝 0)

exact? tells me that it is fun _ a ↦ h (hf a), it is also map_mono h |>.trans hf but none feel right to me...

[Anatole Dedecker]

docs#Filter.Tendsto.mono_left ?