Theorems · Theorem · logic and foundations

Set.definable_biUnion_finset

∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {ι : Type u_2}
  {f : ι → Set (α → M)}, (∀ (i : ι), A.Definable L (f i)) → ∀ (s : Finset ι), A.Definable L (⋃ i ∈ s, f i)

Defined in

Mathlib.ModelTheory.Definability

Cited by

0 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.Structure