Definable Sets

This file defines what it means for a set over a first-order structure to be definable.

Main Definitions

• Set.Definable is defined so that A.Definable L s indicates that the set s of a finite Cartesian power of M is definable with parameters in A.
• Set.Definable₁ is defined so that A.Definable₁ L s indicates that (s : Set M) is definable with parameters in A.
• Set.Definable₂ is defined so that A.Definable₂ L s indicates that (s : Set (M × M)) is definable with parameters in A.
• A FirstOrder.Language.DefinableSet is defined so that L.DefinableSet A α is the Boolean algebra of subsets of α → M defined by formulas with parameters in A.
• Set.TermDefinable functions are those equivalent to some term expressible in the language.
• Set.TermDefinable₁ specialize this to case of unary functions.

Main Results

• L.DefinableSet A α forms a BooleanAlgebra
• Set.Definable.image_comp shows that definability is closed under projections in finite dimensions.
• The Set.TermDefinable property is transitive, and TermDefinable functions are closed under composition.

def Set.Definable {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M] {α : Type u₁} (s : Set (α → M)) : Prop

A subset of a finite Cartesian product of a structure is definable over a set A when membership in the set is given by a first-order formula with parameters from A.

Equations

• A.Definable L s = ∃ (φ : (L.withConstants ↑A).Formula α), s = setOf φ.Realize

theorem Set.Definable.map_expansion {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (α → M)} {L' : FirstOrder.Language} [L'.Structure M] (h : A.Definable L s) (φ : L →ᴸ L') [φ.IsExpansionOn M] : A.Definable L' s

theorem Set.definable_iff_exists_formula_sum {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (α → M)} : A.Definable L s ↔ ∃ (φ : L.Formula (↑A ⊕ α)), s = {v : α → M | φ.Realize (Sum.elim Subtype.val v)}

theorem Set.empty_definable_iff {M : Type w} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (α → M)} : ∅.Definable L s ↔ ∃ (φ : L.Formula α), s = setOf φ.Realize

theorem Set.definable_iff_empty_definable_with_params {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (α → M)} : A.Definable L s ↔ ∅.Definable (L.withConstants ↑A) s

theorem Set.Definable.mono {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {B : Set M} {s : Set (α → M)} (hAs : A.Definable L s) (hAB : A ⊆ B) : B.Definable L s

@[simp]

theorem Set.definable_empty {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} : A.Definable L ∅

@[simp]

theorem Set.definable_univ {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} : A.Definable L univ

@[simp]

theorem Set.Definable.inter {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) : A.Definable L (f ∩ g)

@[simp]

theorem Set.Definable.union {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) : A.Definable L (f ∪ g)

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

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

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

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

theorem Set.definable_iInter_of_finite {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {ι : Type u_2} [Finite ι] {f : ι → Set (α → M)} (hf : ∀ (i : ι), A.Definable L (f i)) : A.Definable L (⋂ (i : ι), f i)

theorem Set.definable_iUnion_of_finite {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {ι : Type u_2} [Finite ι] {f : ι → Set (α → M)} (hf : ∀ (i : ι), A.Definable L (f i)) : A.Definable L (⋃ (i : ι), f i)

@[simp]

theorem Set.Definable.compl {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (α → M)} (hf : A.Definable L s) : A.Definable L sᶜ

@[simp]

theorem Set.Definable.sdiff {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s t : Set (α → M)} (hs : A.Definable L s) (ht : A.Definable L t) : A.Definable L (s \ t)

@[simp]

theorem Set.Definable.himp {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s t : Set (α → M)} (hs : A.Definable L s) (ht : A.Definable L t) : A.Definable L (s ⇨ t)

theorem Set.Definable.preimage_comp {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {β : Type u_1} (f : α → β) {s : Set (α → M)} (h : A.Definable L s) : A.Definable L ((fun (g : β → M) => g ∘ f) ⁻¹' s)

theorem Set.Definable.image_comp_equiv {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {β : Type u_1} {s : Set (β → M)} (h : A.Definable L s) (f : α ≃ β) : A.Definable L ((fun (g : β → M) => g ∘ ⇑f) '' s)

theorem Set.definable_iff_finitely_definable {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (α → M)} : A.Definable L s ↔ ∃ (A0 : Finset M), ↑A0 ⊆ A ∧ (↑A0).Definable L s

theorem Set.Definable.image_comp_sumInl_fin {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} (m : ℕ) {s : Set (α ⊕ Fin m → M)} (h : A.Definable L s) : A.Definable L ((fun (g : α ⊕ Fin m → M) => g ∘ Sum.inl) '' s)

This lemma is only intended as a helper for Definable.image_comp.

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

Shows that definability is closed under finite projections.

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

Shows that definability is closed under finite projections.

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

Finite existential quantifiers preserve definablity.

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

Finite universal quantifiers preserve definablity.

def Set.Definable₁ {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M] (s : Set M) : Prop

A 1-dimensional version of Definable, for Set M.

Equations

• A.Definable₁ L s = A.Definable L {x : Fin 1 → M | x 0 ∈ s}

def Set.Definable₂ {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M] (s : Set (M × M)) : Prop

A 2-dimensional version of Definable, for Set (M × M).

Equations

• A.Definable₂ L s = A.Definable L {x : Fin 2 → M | (x 0, x 1) ∈ s}

theorem Set.Definable.singleton {M : Type w} (L : FirstOrder.Language) [L.Structure M] (a : M) : {a}.Definable₁ L {a}

A singleton is definable by parameter as itself.

theorem Set.Definable.singleton_of_mem {M : Type w} (L : FirstOrder.Language) [L.Structure M] {a : M} {A : Set M} (ha : a ∈ A) : A.Definable₁ L {a}

A singleton {a} is definable over any set A that contains a.

theorem Set.Definable.diagonal {M : Type w} (L : FirstOrder.Language) [L.Structure M] (A : Set M) : A.Definable₂ L (Set.diagonal M)

The 2-dimensional diagonal is definable independent from parameters.

def FirstOrder.Language.DefinableSet (L : Language) {M : Type w} [L.Structure M] (A : Set M) (α : Type u₁) : Type (max 0 u₁ w)

Definable sets are subsets of finite Cartesian products of a structure such that membership is given by a first-order formula.

Equations

• L.DefinableSet A α = { s : Set (α → M) // A.Definable L s }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instSetLike {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : SetLike (L.DefinableSet A α) (α → M)

Equations

• FirstOrder.Language.DefinableSet.instSetLike = { coe := Subtype.val, coe_injective := ⋯ }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instPartialOrder {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : PartialOrder (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instPartialOrder = PartialOrder.ofSetLike (L.DefinableSet A α) (α → M)

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instTop {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : Top (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instTop = { top := ⟨⊤, ⋯⟩ }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instBot {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : Bot (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instBot = { bot := ⟨⊥, ⋯⟩ }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instSup {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : Max (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instSup = { max := fun (s t : L.DefinableSet A α) => ⟨↑s ∪ ↑t, ⋯⟩ }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instInf {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : Min (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instInf = { min := fun (s t : L.DefinableSet A α) => ⟨↑s ∩ ↑t, ⋯⟩ }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instCompl {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : Compl (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instCompl = { compl := fun (s : L.DefinableSet A α) => ⟨(↑s)ᶜ, ⋯⟩ }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instSDiff {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : SDiff (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instSDiff = { sdiff := fun (s t : L.DefinableSet A α) => ⟨↑s \ ↑t, ⋯⟩ }

@[instance_reducible]

noncomputable instance FirstOrder.Language.DefinableSet.instHImp {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : HImp (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instHImp = { himp := fun (s t : L.DefinableSet A α) => ⟨↑s ⇨ ↑t, ⋯⟩ }

@[instance_reducible]

instance FirstOrder.Language.DefinableSet.instInhabited {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : Inhabited (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instInhabited = { default := ⊥ }

theorem FirstOrder.Language.DefinableSet.le_iff {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α} : s ≤ t ↔ ↑s ⊆ ↑t

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_top {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {x : α → M} : x ∈ ⊤

@[simp]

theorem FirstOrder.Language.DefinableSet.notMem_bot {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {x : α → M} : x ∉ ⊥

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_sup {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α} {x : α → M} : x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_inf {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α} {x : α → M} : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_compl {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s : L.DefinableSet A α} {x : α → M} : x ∈ sᶜ ↔ x ∉ s

@[simp]

theorem FirstOrder.Language.DefinableSet.mem_sdiff {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s t : L.DefinableSet A α} {x : α → M} : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_top {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : ↑⊤ = Set.univ

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_bot {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : ↑⊥ = ∅

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_sup {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α) : ↑(s ⊔ t) = ↑s ∪ ↑t

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_inf {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_compl {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s : L.DefinableSet A α) : ↑sᶜ = (↑s)ᶜ

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_sdiff {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α) : ↑(s \ t) = ↑s \ ↑t

@[simp]

theorem FirstOrder.Language.DefinableSet.coe_himp {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s t : L.DefinableSet A α) : ↑(s ⇨ t) = ↑s ⇨ ↑t

@[instance_reducible]

noncomputable instance FirstOrder.Language.DefinableSet.instBooleanAlgebra {L : Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} : BooleanAlgebra (L.DefinableSet A α)

Equations

• FirstOrder.Language.DefinableSet.instBooleanAlgebra = Function.Injective.booleanAlgebra (fun (a : { s : Set (α → M) // A.Definable L s }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def Set.DefinableFun {M : Type u_1} (L : FirstOrder.Language) [L.Structure M] {α : Type u_2} (A : Set M) (f : (α → M) → M) : Prop

A function from tuples of elements of M to M is definable if its graph is definable.

Equations

• Set.DefinableFun L A f = A.Definable L (Function.tupleGraph f)

def Set.DefinableMap {M : Type u_1} (L : FirstOrder.Language) [L.Structure M] {α : Type u_2} {β : Type u_3} (A : Set M) (F : (α → M) → β → M) : Prop

A family of functions is definable when each coordinate is definable.

Equations

• Set.DefinableMap L A F = ∀ (i : β), Set.DefinableFun L A fun (x : α → M) => F x i

theorem Set.DefinableFun.mono {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M} {B : Set M} (hAs : DefinableFun L A f) (hAB : A ⊆ B) : DefinableFun L B f

theorem Set.DefinableFun.of_empty {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M} (hAs : DefinableFun L ∅ f) : DefinableFun L A f

theorem Set.empty_definableFun_iff {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {f : (α → M) → M} : DefinableFun L ∅ f ↔ ∃ (φ : L.Formula (Option α)), Function.tupleGraph f = setOf φ.Realize

theorem Set.definableFun_iff_empty_definableFun_with_params {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M} : DefinableFun L A f ↔ DefinableFun (L.withConstants ↑A) ∅ f

theorem FirstOrder.Language.Term.definableFun_realize {M : Type u_1} {L : Language} [L.Structure M] {α : Type u_2} (t : L.Term α) : Set.DefinableFun L ∅ fun (v : α → M) => realize v t

A term is a definable function.

theorem Set.DefinableFun.fun_symbol {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {n : ℕ} (f : L.Functions n) : DefinableFun L ∅ (FirstOrder.Language.Structure.funMap f)

A function symbol is a definable function.

theorem FirstOrder.Language.definableFun_var {M : Type u_1} (L : Language) [L.Structure M] {α : Type u_2} (i : α) : Set.DefinableFun L ∅ fun (v : α → M) => v i

A coordinate projection is a definable function.

theorem Set.DefinableFun.proj {M : Type u_1} (L : FirstOrder.Language) [L.Structure M] {α : Type u_2} {A : Set M} {i : α} : DefinableFun L A fun (v : α → M) => v i

theorem FirstOrder.Language.definableFun_const {M : Type u_1} (L : Language) [L.Structure M] {A : Set M} {a : M} (γ : Type u_4) (ha : a ∈ A) : Set.DefinableFun L A fun (x : γ → M) => a

A constant function is a definable function.

theorem Set.Definable.preimage_map {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {A : Set M} {α : Type u_4} {β : Type u_5} [Finite β] {F : (α → M) → β → M} (hF : DefinableMap L A F) {S : Set (β → M)} (hS : A.Definable L S) : A.Definable L (F ⁻¹' S)

The preimage of a definable set under a definable map is definable.

theorem Set.DefinableFun.comp {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {β : Type u_3} {A : Set M} {f : (α → M) → M} [Finite α] {g : (β → M) → α → M} (hg : DefinableMap L A g) (hf : DefinableFun L A f) : DefinableFun L A fun (v : β → M) => f (g v)

theorem Set.DefinableFun.ite {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M} {p : (α → M) → Prop} {g : (α → M) → M} [DecidablePred p] (hp : A.Definable L (setOf p)) (hf : DefinableFun L A f) (hg : DefinableFun L A g) : DefinableFun L A fun (v : α → M) => if p v then f v else g v

theorem Set.DefinableFun.setOf_eq {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {A : Set M} {f g : (α → M) → M} (hf : DefinableFun L A f) (hg : DefinableFun L A g) : A.Definable L {v : α → M | f v = g v}

The set where two definable functions agree is definable.

theorem Set.DefinableFun.setOf_eq_const {M : Type u_1} {L : FirstOrder.Language} [L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M} (hf : DefinableFun L A f) {a : M} (ha : a ∈ A) : A.Definable L {v : α → M | f v = a}

The preimage of a constant under a definable function is definable.

def Set.TermDefinable {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M] {α : Type u₁} (f : (α → M) → M) : Prop

A function from a Cartesian power of a structure to that structure is term-definable over a set A when the value of the function is given by a term with constants A.

Equations

• A.TermDefinable L f = ∃ (φ : (L.withConstants ↑A).Term α), f = fun (v : α → M) => FirstOrder.Language.Term.realize v φ

theorem Set.TermDefinable.definable_tupleGraph {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M] {α : Type u₁} {f : (α → M) → M} (h : A.TermDefinable L f) : A.Definable L (Function.tupleGraph f)

Every TermDefinable function has a tupleGraph that is definable.

theorem Set.TermDefinable.map_expansion {M : Type w} {A : Set M} {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.Structure M] [L'.Structure M] {α : Type u₁} {f : (α → M) → M} (h : A.TermDefinable L f) (φ : L →ᴸ L') [φ.IsExpansionOn M] : A.TermDefinable L' f

theorem Set.termDefinable_empty_iff {M : Type w} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {f : (α → M) → M} : ∅.TermDefinable L f ↔ ∃ (φ : L.Term α), f = fun (v : α → M) => FirstOrder.Language.Term.realize v φ

theorem Set.termDefinable_empty_withConstants_iff {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {f : (α → M) → M} : ∅.TermDefinable (L.withConstants ↑A) f ↔ A.TermDefinable L f

theorem Set.TermDefinable.mono {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {B : Set M} {f : (α → M) → M} (h : A.TermDefinable L f) (hAB : A ⊆ B) : B.TermDefinable L f

theorem Set.TermDefinable.trans {M : Type w} {A : Set M} {L : FirstOrder.Language} {L' : FirstOrder.Language} [L.Structure M] [L'.Structure M] {β : Type u_1} {f : (β → M) → M} (h₁ : A.TermDefinable L f) (h₂ : ∀ {n : ℕ} (g : (L.withConstants ↑A).Functions n), A.TermDefinable L' fun (v : Fin n → M) => FirstOrder.Language.Term.realize v g.term) : A.TermDefinable L' f

TermDefinable is transitive. If f is TermDefinable in a structure S on L, and all of the functions' realizations on S are TermDefinable on a structure T on L', then f is TermDefinable on T in L'.

def Set.TermDefinable₁ {M : Type w} {A : Set M} (L : FirstOrder.Language) [L.Structure M] (f : M → M) : Prop

A function from a structure to itself is term-definable over a set A when the value of the function is given by a term with constants A. Like TermDefinable but specialized for unary functions in order to write M → M instead of (Unit → M) → M.

Equations

• Set.TermDefinable₁ L f = A.TermDefinable L fun (x : Unit → M) => f (x ())

theorem Set.termDefinable₁_iff_termDefinable {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] (f : M → M) : TermDefinable₁ L f ↔ A.TermDefinable L fun (v : Unit → M) => f (v ())

TermDefinable₁ is defined as TermDefinable on the Unit index type.

theorem Set.TermDefinable.termDefinable₁ {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] (f : M → M) : (A.TermDefinable L fun (v : Unit → M) => f (v ())) → TermDefinable₁ L f

Alias of the reverse direction of Set.termDefinable₁_iff_termDefinable.

---

TermDefinable₁ is defined as TermDefinable on the Unit index type.

theorem Set.TermDefinable₁.termDefinable {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] (f : M → M) : TermDefinable₁ L f → A.TermDefinable L fun (v : Unit → M) => f (v ())

Alias of the forward direction of Set.termDefinable₁_iff_termDefinable.

---

TermDefinable₁ is defined as TermDefinable on the Unit index type.

theorem Set.termDefinable₁_iff_exists_term {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {f : M → M} : TermDefinable₁ L f ↔ ∃ (φ : (L.withConstants ↑A).Term Unit), f = (fun (v : Unit → M) => FirstOrder.Language.Term.realize v φ) ∘ Function.const Unit

theorem Set.TermDefinable₁.definable₂_graph {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {f : M → M} (h : TermDefinable₁ L f) : A.Definable₂ L (Function.graph f)

A TermDefinable₁ function has a graph that's Definable₂.

theorem Set.TermDefinable₁.id {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] : TermDefinable₁ L _root_.id

The identity function is TermDefinable₁

theorem Set.TermDefinable.const {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} (C : (L.withConstants ↑A).Constants) : A.TermDefinable L (Function.const (α → M) ↑C)

Constant functions are TermDefinable, assuming the constant value is a language constant.

theorem Set.TermDefinable₁.const {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] (C : (L.withConstants ↑A).Constants) : TermDefinable₁ L (Function.const M ↑C)

Constant functions are TermDefinable₁, assuming the constant value is a language constant.

theorem Set.TermDefinable.comp {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {β : Type u_1} {f : (α → M) → M} {g : α → (β → M) → M} (hf : A.TermDefinable L f) (hg : ∀ (i : α), A.TermDefinable L (g i)) : A.TermDefinable L fun (b : β → M) => f fun (x : α) => g x b

A k-ary TermDefinable function composed with k TermDefinable others is TermDefinable.

theorem Set.TermDefinable₁.comp {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {f g : M → M} (hf : TermDefinable₁ L f) (hg : TermDefinable₁ L g) : TermDefinable₁ L (f ∘ g)

TermDefinable₁ functions are closed under composition.

theorem Set.TermDefinable₁.comp_termDefinable {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {f : M → M} {g : (α → M) → M} (hf : TermDefinable₁ L f) (hg : A.TermDefinable L g) : A.TermDefinable L (f ∘ g)

A TermDefinable function postcomposed with TermDefinable₁ is TermDefinable.