sUnion — Mathlib

English

Let S be a finite set of subsets of X such that each member is locally constructible; then the union of all sets in S is locally constructible.

Русский

Пусть S — конечное множество подмножеств X, каждый элемент которого локально конструируем; тогда объединение всех множеств из S локально конструируемо.

LaTeX

$$$\\#S<\\infty \\ \\wedge\\ \\forall s\\in S, \\operatorname{IsLocallyConstructible}(s) \\;\\Rightarrow\\; \\operatorname{IsLocallyConstructible}\\left(\\bigcup S\\right).$$$

Lean4

theorem sUnion {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsLocallyConstructible s) :
    IsLocallyConstructible (⋃₀ S) :=
  SupClosed.sSup_mem (s := {s | IsLocallyConstructible s}) (fun _ h₁ _ ↦ h₁.union) hS .empty hS'

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