tendstoIxxClass_of_subset — Mathlib

English

If a pointwise subset relation h: Ixx a b ⊆ Ixx' a b holds for all a,b, then TendstoIxxClass Ixx l1 l2 follows from TendstoIxxClass Ixx' l1 l2.

Русский

Если для всех a,b выполняется включение Ixx a b ⊆ Ixx' a b, то из TendstoIxxClass Ixx' l1 l2 следует TendstoIxxClass Ixx l1 l2.

LaTeX

$$$(\\forall a,b,\\ Ixx\\ a\\ b \\subseteq Ixx'\\ a\\ b) \\Rightarrow (\\text{TendstoIxxClass } Ixx'\\ l_1\\ l_2 \\Rightarrow \\text{TendstoIxxClass } Ixx\\ l_1\\ l_2)$$$

Lean4

theorem tendstoIxxClass_of_subset {l₁ l₂ : Filter α} {Ixx Ixx' : α → α → Set α} (h : ∀ a b, Ixx a b ⊆ Ixx' a b)
    [h' : TendstoIxxClass Ixx' l₁ l₂] : TendstoIxxClass Ixx l₁ l₂ :=
  ⟨h'.1.smallSets_mono <| Eventually.of_forall <| Prod.forall.2 h⟩

Похожие утверждения