piecewise — Mathlib

English

If Tendsto f (l1 ∩ 𝓟 s) l2 and Tendsto g (l1 ∩ 𝓟 sᶜ) l2, then Tendsto (s.piecewise f g) l1 l2.

Русский

Если Tendsto f на l1 ∩ 𝓟 s в l2 и Tendsto g на l1 ∩ 𝓟 sᶜ в l2, то Tendsto s.piecewise f g от l1 в l2.

LaTeX

$$$ \\operatorname{Tendsto} f (l_1 \\cap 𝓟 s) l_2 \\; \\land \\; \\operatorname{Tendsto} g (l_1 \\cap 𝓟 s^c) l_2 \\Rightarrow \\operatorname{Tendsto} (s.piecewise f g) l_1 l_2 $$$

Lean4

protected theorem piecewise {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {s : Set α} [∀ x, Decidable (x ∈ s)]
    (h₀ : Tendsto f (l₁ ⊓ 𝓟 s) l₂) (h₁ : Tendsto g (l₁ ⊓ 𝓟 sᶜ) l₂) : Tendsto (piecewise s f g) l₁ l₂ :=
  Tendsto.if h₀ h₁

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