English
There is a Tendsto relation for the uIcc construction that lifts the Icc Tendsto property to the uIcc level in a linear order.
Русский
Существует отношение Tendsto для конструкции uIcc, поднимающее свойство Tendsto для Icc на уровень uIcc в линейном порядке.
LaTeX
$$$$ \operatorname{TendstoIxxClass}(\mathrm{uIcc}, \mathcal{P}(\mathrm{[[a,b]]}), \mathcal{P}(\mathrm{[[a,b]]})) $$$$
Lean4
protected theorem uIcc {l : Filter α} [TendstoIxxClass Icc l l] {f g : β → α} {lb : Filter β} (hf : Tendsto f lb l)
(hg : Tendsto g lb l) : Tendsto (fun x => [[f x, g x]]) lb l.smallSets :=
(@TendstoIxxClass.tendsto_Ixx α Set.uIcc _ _ _).comp <| hf.prodMk hg
