English
If f1, f2 converge to p1, p2 respectively and g converges to c, then the line map of f1, f2, g converges to the line map of p1, p2, c.
Русский
Если f1→p1 и f2→p2, и g→c, то отображение lineMap(f1, f2, g) сходится к lineMap(p1, p2, c).
LaTeX
$$$\text{Tendsto}(f_1,l,nhds(p_1)) \to \text{Tendsto}(f_2,l,nhds(p_2)) \to \text{Tendsto}(g,l,nhds(c)) \Rightarrow \text{Tendsto}(\lambda x. lineMap(f_1(x),f_2(x),g(x)),l,nhds(lineMap(p_1,p_2,c)))$$$
Lean4
theorem _root_.Filter.Tendsto.lineMap {f₁ f₂ : α → P} {g : α → R} {p₁ p₂ : P} {c : R} (h₁ : Tendsto f₁ l (𝓝 p₁))
(h₂ : Tendsto f₂ l (𝓝 p₂)) (hg : Tendsto g l (𝓝 c)) :
Tendsto (fun x => AffineMap.lineMap (f₁ x) (f₂ x) (g x)) l (𝓝 <| AffineMap.lineMap p₁ p₂ c) :=
(hg.smul (h₂.vsub h₁)).vadd h₁
