English
There is a general criterion characterizing TendstoIxxClass Ixx l l by a universal property on the underlying relation Ixx.
Русский
Существует общая характеристика TendstoIxxClass Ixx l l через универсальное свойство для отношения Ixx.
LaTeX
$$$(\\forall l, l', Ixx) \\ (TendstoIxxClass Ixx l l' \\text{ iff } \\text{(appropriate a priori condition)})$$$
Lean4
protected theorem Icc {l₁ l₂ : Filter α} [TendstoIxxClass Icc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α}
(h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Icc (u₁ x) (u₂ x)) lb l₂.smallSets :=
(@TendstoIxxClass.tendsto_Ixx α Set.Icc _ _ _).comp <| h₁.prodMk h₂
