mathlib documentation

model_theory.definability

Definable Sets #

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

Main Definitions #

Main Results #

def set.definable {M : Type w} (A : set M) (L : first_order.language) [L.Structure M] {α : Type u_1} (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
theorem set.definable.map_expansion {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set (α → M)} {L' : first_order.language} [L'.Structure M] (h : A.definable L s) (φ : L →ᴸ L') [φ.is_expansion_on M] :
A.definable L' s
theorem set.empty_definable_iff {M : Type w} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set (α → M)} :
.definable L s ∃ (φ : L.formula α), s = set_of φ.realize
theorem set.definable_iff_empty_definable_with_params {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set (α → M)} :
theorem set.definable.mono {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {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 : first_order.language} [L.Structure M] {α : Type u_1} :
@[simp]
theorem set.definable_univ {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} :
@[simp]
theorem set.definable.inter {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {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 : first_order.language} [L.Structure M] {α : Type u_1} {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 : first_order.language} [L.Structure M] {α : Type u_1} {ι : 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 : first_order.language} [L.Structure M] {α : Type u_1} {ι : Type u_2} {f : ι → set (α → M)} (hf : ∀ (i : ι), A.definable L (f i)) (s : finset ι) :
A.definable L (s.sup f)
theorem set.definable_finset_bInter {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {ι : Type u_2} {f : ι → set (α → M)} (hf : ∀ (i : ι), A.definable L (f i)) (s : finset ι) :
A.definable L (⋂ (i : ι) (H : i s), f i)
theorem set.definable_finset_bUnion {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {ι : Type u_2} {f : ι → set (α → M)} (hf : ∀ (i : ι), A.definable L (f i)) (s : finset ι) :
A.definable L (⋃ (i : ι) (H : i s), f i)
@[simp]
theorem set.definable.compl {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {s : set (α → M)} (hf : A.definable L s) :
@[simp]
theorem set.definable.sdiff {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {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 : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} (f : α → β) {s : set (α → M)} (h : A.definable L s) :
A.definable L ((λ (g : β → M), g f) ⁻¹' s)
theorem set.definable.image_comp_equiv {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} {s : set (β → M)} (h : A.definable L s) (f : α β) :
A.definable L ((λ (g : β → M), g f) '' s)
theorem set.definable.image_comp_sum_inl_fin {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} (m : ) {s : set fin m → M)} (h : A.definable L s) :
A.definable L ((λ (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 : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} {s : set (β → M)} (h : A.definable L s) (f : α β) [fintype β] :
A.definable L ((λ (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 : first_order.language} [L.Structure M] {α : Type u_1} {β : Type u_2} {s : set (β → M)} (h : A.definable L s) (f : α → β) [fintype α] [fintype β] :
A.definable L ((λ (g : β → M), g f) '' s)

Shows that definability is closed under finite projections.

def set.definable₁ {M : Type w} (A : set M) (L : first_order.language) [L.Structure M] (s : set M) :
Prop

A 1-dimensional version of definable, for set M.

Equations
def set.definable₂ {M : Type w} (A : set M) (L : first_order.language) [L.Structure M] (s : set (M × M)) :
Prop

A 2-dimensional version of definable, for set (M × M).

Equations
@[protected, instance]
def first_order.language.definable_set.has_top {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
Equations
@[protected, instance]
def first_order.language.definable_set.has_bot {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
Equations
@[protected, instance]
def first_order.language.definable_set.inhabited {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
Equations
@[protected, instance]
def first_order.language.definable_set.pi.set_like {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
set_like (L.definable_set A α) (α → M)
Equations
@[simp]
theorem first_order.language.definable_set.mem_top {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {x : α → M} :
@[simp]
theorem first_order.language.definable_set.coe_top {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
@[simp]
theorem first_order.language.definable_set.not_mem_bot {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {x : α → M} :
@[simp]
theorem first_order.language.definable_set.coe_bot {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
@[protected, instance]
def first_order.language.definable_set.lattice {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
Equations
theorem first_order.language.definable_set.le_iff {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : L.definable_set A α} :
s t s t
@[simp]
theorem first_order.language.definable_set.coe_sup {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : L.definable_set A α} :
(s t) = s t
@[simp]
theorem first_order.language.definable_set.mem_sup {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : L.definable_set A α} {x : α → M} :
x s t x s x t
@[simp]
theorem first_order.language.definable_set.coe_inf {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : L.definable_set A α} :
(s t) = s t
@[simp]
theorem first_order.language.definable_set.mem_inf {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s t : L.definable_set A α} {x : α → M} :
x s t x s x t
@[protected, instance]
def first_order.language.definable_set.bounded_order {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
Equations
@[protected, instance]
def first_order.language.definable_set.has_compl {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :

The complement of a definable set is also definable.

Equations
@[simp]
theorem first_order.language.definable_set.mem_compl {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s : L.definable_set A α} {x : α → M} :
x s x s
@[simp]
theorem first_order.language.definable_set.coe_compl {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} {s : L.definable_set A α} :