English
If h0 and h1 are Tendsto statements for f and g restricted to complementary parts of a set, then Tendsto of the piecewise function holds.
Русский
Если для разбиения на две части множества s верны схождения h0 и h1 для функций f и g соответственно, то сходится кусочно-заданная функция.
LaTeX
$$$ \\text{Tendsto} f (l_1 \\cap 𝓟 s) \\; l_2 \\land \\text{Tendsto} g (l_1 \\cap 𝓟 s^c) \\; l_2 \\Rightarrow \\text{Tendsto} (\\lambda x. \\mathbf{if} \\; p x \\; \\mathbf{then} f x \\mathbf{else} g x) l_1 l_2 $$$
Lean4
protected theorem «if» {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop} [∀ x, Decidable (p x)]
(h₀ : Tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂) (h₁ : Tendsto g (l₁ ⊓ 𝓟 {x | ¬p x}) l₂) :
Tendsto (fun x => if p x then f x else g x) l₁ l₂ :=
by
simp only [tendsto_def, mem_inf_principal] at *
intro s hs
filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁
rw [mem_preimage]
split_ifs with h
exacts [hp₀ h, hp₁ h]
