Theorems · Theorem · logic and foundations

Set.Definable.forall_of_finite

∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1} [Finite β]
  {S : Set (α ⊕ β → M)}, A.Definable L S → A.Definable L {v | ∀ (u : β → M), Sum.elim v u ∈ S}

Finite universal quantifiers preserve definablity.

Defined in

Mathlib.ModelTheory.Definability

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFinite