Theorems · Theorem · logic and foundations

Set.Definable.image_comp_embedding

∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
  {s : Set (β → M)}, A.Definable L s → ∀ (f : α ↪ β) [Finite β], A.Definable L ((fun g => g ∘ ⇑f) '' s)

Shows that definability is closed under finite projections.

Defined in

Mathlib.ModelTheory.Definability

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFinite