English
For any α, β, and a relation Ixx on α, the following is equivalent: TendstoIxxClass Ixx (principal s) (principal t) holds if and only if almost every pair x,y in s satisfies Ixx x y ⊆ t.
Русский
Для любой пары множеств s, t в α и отношения Ixx по α верно: TendstoIxxClass Ixx (principal s) (principal t) эквивалентно тому, что для почти всех пар x,y в s выполняется Ixx x y ⊆ t.
LaTeX
$$$\\mathrm{TendstoIxxClass}\\ Ixx\\ (\\mathcal{P} s)\\ (\\mathcal{P} t) \\iff \\forall^\\infty (x\\in s)(y\\in s),\\ Ixx\\ x\\ y\\subseteq t$$$
Lean4
theorem tendstoIxxClass_principal {s t : Set α} {Ixx : α → α → Set α} :
TendstoIxxClass Ixx (𝓟 s) (𝓟 t) ↔ ∀ᵉ (x ∈ s) (y ∈ s), Ixx x y ⊆ t :=
Iff.trans ⟨fun h => h.1, fun h => ⟨h⟩⟩ <| by
simp only [smallSets_principal, prod_principal_principal, tendsto_principal_principal, forall_prod_set,
mem_powerset_iff]
