English
If Tendsto f l1 l2 and Tendsto g l1 l2, then Tendsto (fun a => if p a then f a else g a) l1 l2.
Русский
Если Tendsto f l1 l2 и Tendsto g l1 l2, тогда Tendsto (функция, равная f на p и g иначе) l1 l2.
LaTeX
$$$ \\operatorname{Tendsto} f l_1 l_2 \\rightarrow \\operatorname{Tendsto} g l_1 l_2 \\rightarrow \\operatorname{Tendsto} (\\lambda a. \\mathbf{ITE} (p a) (f a) (g a)) l_1 l_2 $$$
Lean4
protected theorem if' {α β : Type*} {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop} [DecidablePred p]
(hf : Tendsto f l₁ l₂) (hg : Tendsto g l₁ l₂) : Tendsto (fun a => if p a then f a else g a) l₁ l₂ :=
(tendsto_inf_left hf).if (tendsto_inf_left hg)
