Ioo — Mathlib

English

If h₁,h₂ are Tendsto of u₁,u₂ to l₁, then Tendsto (x ↦ Ioo(u₁ x, u₂ x)) lb l₂.smallSets.

Русский

Если h₁,h₂ являются пределами перехода функций u₁,u₂ к l₁, то Tendsto (x ↦ Ioo(u₁ x, u₂ x)) достигает l₂.smallSets.

LaTeX

$$$\\text{Tendsto } (x \\mapsto Ioo(u_1 x, u_2 x))\\ lb\\ l_2^{\\text{smallSets}}$$$

Lean4

protected theorem Ioo {l₁ l₂ : Filter α} [TendstoIxxClass Ioo l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α}
    (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Ioo (u₁ x) (u₂ x)) lb l₂.smallSets :=
  (@TendstoIxxClass.tendsto_Ixx α Set.Ioo _ _ _).comp <| h₁.prodMk h₂

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