Definable Sets #
This file defines what it means for a set over a first-order structure to be definable.
Main Definitions #
Set.Definableis defined so thatA.Definable L sindicates that the setsof a finite Cartesian power ofMis definable with parameters inA.Set.Definable₁is defined so thatA.Definable₁ L sindicates that(s : Set M)is definable with parameters inA.Set.Definable₂is defined so thatA.Definable₂ L sindicates that(s : Set (M × M))is definable with parameters inA.- A
FirstOrder.Language.DefinableSetis defined so thatL.DefinableSet A αis the Boolean algebra of subsets ofα → Mdefined by formulas with parameters inA. Set.TermDefinablefunctions 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 aBooleanAlgebraSet.Definable.image_compshows that definability is closed under projections in finite dimensions.- The
Set.TermDefinableproperty is transitive, andTermDefinablefunctions are closed under composition.
def
Set.Definable
{M : Type w}
(A : Set M)
(L : FirstOrder.Language)
[L.Structure M]
{α : Type u₁}
(s : Set (α → M))
:
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.
Instances For
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_empty_definable_with_params
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
{s : Set (α → M)}
:
@[simp]
theorem
Set.definable_empty
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
:
@[simp]
theorem
Set.definable_univ
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
:
@[deprecated Set.definable_biInter_finset (since := "2025-08-28")]
theorem
Set.definable_finset_biInter
{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)
Alias of Set.definable_biInter_finset.
@[deprecated Set.definable_biUnion_finset (since := "2025-08-28")]
theorem
Set.definable_finset_biUnion
{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)
Alias of Set.definable_biUnion_finset.
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)
:
This lemma is only intended as a helper for Definable.image_comp.
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
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
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
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
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, ⋯⟩ }
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
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 := ⊥ }
@[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 α)
:
@[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 α)
:
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.TermDefinable
{M : Type w}
(A : Set M)
(L : FirstOrder.Language)
[L.Structure M]
{α : Type u₁}
(f : (α → M) → M)
:
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 φ
Instances For
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}
:
theorem
Set.termDefinable_empty_withConstants_iff
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
{α : Type u₁}
{f : (α → M) → M}
:
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)
:
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 ())
Instances For
theorem
Set.termDefinable₁_iff_termDefinable
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[L.Structure M]
(f : M → M)
:
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₂.
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.