English
For h₁,h₂: Tendsto u₁ lb l₁ and Tendsto u₂ lb l₁, the function x ↦ Ioc(u₁ x, u₂ x) tends to l₂.smallSets.
Русский
Пусть h₁,h₂: Tendsto u₁ lb l₁ и Tendsto u₂ lb l₁. Тогда x ↦ Ioc(u₁ x, u₂ x) стремится к l₂.smallSets.
LaTeX
$$$\\text{Tendsto } (x \\mapsto Ioc(u_1 x, u_2 x))\\ lb\\ l_2^{\\text{smallSets}}$$$
Lean4
protected theorem Ioc {l₁ l₂ : Filter α} [TendstoIxxClass Ioc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α}
(h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Ioc (u₁ x) (u₂ x)) lb l₂.smallSets :=
(@TendstoIxxClass.tendsto_Ixx α Set.Ioc _ _ _).comp <| h₁.prodMk h₂