English
If f1 → p1 and f2 → p2, then the midpoint of f1 and f2 tends to the midpoint of p1 and p2, provided 2 is invertible.
Русский
Если f1 → p1 и f2 → p2, то середина(midpoint) f1 и f2 сходится к середине p1 и p2, при условии обратимости 2 в кольце.
LaTeX
$$$\text{Tendsto}(f_1,l,nhds(p_1)) \to \text{Tendsto}(f_2,l,nhds(p_2)) \Rightarrow \text{Tendsto}(\lambda x. midpoint_R(f_1(x),f_2(x)),l,nhds(midpoint_R(p_1,p_2)))$$$
Lean4
theorem _root_.Filter.Tendsto.midpoint [Invertible (2 : R)] {f₁ f₂ : α → P} {p₁ p₂ : P} (h₁ : Tendsto f₁ l (𝓝 p₁))
(h₂ : Tendsto f₂ l (𝓝 p₂)) : Tendsto (fun x => midpoint R (f₁ x) (f₂ x)) l (𝓝 <| midpoint R p₁ p₂) :=
h₁.lineMap h₂ tendsto_const_nhds
