English
If l has a basis indexed by p and s, and H ensures Ixx maps inside s, then TendstoIxxClass Ixx l l holds.
Русский
Если у фильтра l есть базис, индексируемый p и s, и условие H обеспечивает вложение Ixx внутрь s, тогда выполняется TendstoIxxClass Ixx l l.
LaTeX
$$$\\text{HasBasis }(l) \\Rightarrow (\\forall i, p(i) \\Rightarrow \\forall x\\in s(i), \\forall y\\in s(i), Ixx x y \\subseteq s(i)) \\Rightarrow \\text{TendstoIxxClass } Ixx l l$$$
Lean4
theorem tendstoIxxClass {ι : Type*} {p : ι → Prop} {s} {l : Filter α} (hl : l.HasBasis p s) {Ixx : α → α → Set α}
(H : ∀ i, p i → ∀ x ∈ s i, ∀ y ∈ s i, Ixx x y ⊆ s i) : TendstoIxxClass Ixx l l :=
⟨(hl.prod_self.tendsto_iff hl.smallSets).2 fun i hi => ⟨i, hi, fun _ h => H i hi _ h.1 _ h.2⟩⟩
