tendstoIxxClass_inf — Mathlib

English

If l1 and l2 have TendstoIxxClass Ixx to l2, then their infimum filter also preserves Ixx: TendstoIxxClass Ixx (l1 ⊓ l1') (l2 ⊓ l2').

Русский

Если существуют два фильтра l1, l1' и l2, l2' с свойством TendstoIxxClass Ixx, то их встречное пересечение сохраняет Ixx: TendstoIxxClass Ixx (l1 ⊓ l1') (l2 ⊓ l2').

LaTeX

$$$\\text{TendstoIxxClass } Ixx (l_1 \\sqcap l_1') (l_2 \\sqcap l_2')$ given the respective hypotheses$$

Lean4

theorem tendstoIxxClass_inf {l₁ l₁' l₂ l₂' : Filter α} {Ixx} [h : TendstoIxxClass Ixx l₁ l₂]
    [h' : TendstoIxxClass Ixx l₁' l₂'] : TendstoIxxClass Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂') :=
  ⟨by simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1⟩

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