if_nhdsWithin — Mathlib

English

If f tends to nhdsWithin a on s ∩ t and g tends to nhdsWithin a on s ∩ t^c, then the piecewise function t.piecewise f g tends to nhdsWithin a on s.

Русский

Если в области s ∩ t функция f сходится к окрестностям a и в области s ∩ t^c функция g сходится к окрестностям a, то piecewise-f(x) сходится к окрестностям a на s.

LaTeX

$$$$\\\\text{Tendsto} (t.Piecewise f g) (\\\\mathcal{N}_{s}(a)) l.$$$$

Lean4

theorem if_nhdsWithin {f g : α → β} {p : α → Prop} [DecidablePred p] {a : α} {s : Set α} {l : Filter β}
    (h₀ : Tendsto f (𝓝[s ∩ {x | p x}] a) l) (h₁ : Tendsto g (𝓝[s ∩ {x | ¬p x}] a) l) :
    Tendsto (fun x => if p x then f x else g x) (𝓝[s] a) l :=
  h₀.piecewise_nhdsWithin h₁

Похожие утверждения