biInter — Mathlib

English

Finite intersection of constructible sets is constructible.

Русский

Конечное пересечение конструктивных множеств является конструктивным.

LaTeX

$$$\text{Finite}(t) \rightarrow (\forall i \in t, \text{IsConstructible}(f(i))) \rightarrow \text{IsConstructible}(\bigcap_{i\in t} f(i))$$$

Lean4

theorem biInter {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite) (hf : ∀ i ∈ t, IsConstructible (f i)) :
    IsConstructible (⋂ i ∈ t, f i) :=
  BooleanSubalgebra.biInf_mem ht hf

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