iInter — Mathlib

English

If a finite family of sets is locally constructible, their intersection is locally constructible.

Русский

Если конечная совокупность множеств локально конструируема, их пересечение локально конструируемо.

LaTeX

$$$IsLocallyConstructible(\\bigcap_{i\\in F} f(i))$ for finite F.$$

Lean4

theorem iInter [Finite ι] {f : ι → Set X} (hf : ∀ i, IsLocallyConstructible (f i)) :
    IsLocallyConstructible (⋂ i, f i) :=
  infClosed_isLocallyConstructible.iInf_mem .univ hf

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