English
If f tends to c within a left-neighborhood, then multiplying by a fixed b preserves the left-neighborhood tendency: Tendsto (a ↦ b · f(a)) l (nhdsWithin (b · c) (Iio(b · c))).
Русский
Если f стремится к c внутри левой окрестности, умножение на константу b сохраняет тенденцию слева: Tendsto (a ↦ b f(a)) l (nhdsWithin (b c) (Iio(b c))).
LaTeX
$$$\text{Tendsto}(f, l, \nhdsWithin c(\{x \mid x < c\})) \Rightarrow \text{Tendsto}(a \mapsto b f(a), l, \nhdsWithin (b c)(\{x \mid x < b c\}))$$$
Lean4
theorem mul_const [MulPosStrictMono 𝕜] (h : Tendsto f l (𝓝[<] c)) : Tendsto (fun a => f a * b) l (𝓝[<] (c * b)) :=
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ((tendsto_nhds_of_tendsto_nhdsWithin h).mul_const b) <|
(tendsto_nhdsWithin_iff.mp h).2.mono fun _ _ => by rw [Set.mem_Iio] at *; gcongr; assumption
