sInter — Mathlib

English

Finite union of locally constructible sets is locally constructible.

Русский

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

LaTeX

$$$IsLocallyConstructible(\\bigcup_{i=1}^n s_i)$$$

Lean4

theorem sInter {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsLocallyConstructible s) :
    IsLocallyConstructible (⋂₀ S) :=
  infClosed_isLocallyConstructible.sInf_mem hS .univ hS'

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