Ico — Mathlib

English

For h₁,h₂: Tendsto u₁ lb l₁ and Tendsto u₂ lb l₁, Tendsto (x ↦ Icc(u₁ x, u₂ x)) lb l₂.smallSets holds.

Русский

Пусть h₁,h₂: Tendsto u₁ lb l₁ и Tendsto u₂ lb l₁. Тогда Tendsto (x ↦ Icc(u₁ x, u₂ x)) lb l₂.smallSets.

LaTeX

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

Lean4

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

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