finsetInf — Mathlib

English

The finite intersection of locally constructible sets is locally constructible.

Русский

Конечная конъюнкция локально конструируемых множеств локально конструируема.

LaTeX

$$$IsLocallyConstructible(\\bigwedge_{i\\in s} t_i)$$$

Lean4

theorem finsetInf {ι : Type*} {s : Finset ι} {t : ι → Set X} (ht : ∀ i ∈ s, IsLocallyConstructible (t i)) :
    IsLocallyConstructible (s.inf t) := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons i s ih hi =>
    rw [Finset.inf_cons]
    exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

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