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₂