mathlib3 documentation

model_theory.definability

Definable Sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines what it means for a set over a first-order structure to be definable.

Main Definitions #

Main Results #

source
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
source
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
source
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
source
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)} :
A.definable L s ↔ ∅.definable (L.with_constants ↥A) s
source
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
source
@[simp]
theorem set.definable_empty {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} :
A.definable L ∅
source
@[simp]
theorem set.definable_univ {M : Type w} {A : set M} {L : first_order.language} [L.Structure M] {α : Type u_1} :
A.definable L set.univ
source
@[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)
source
@[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)
source
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)
source
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)
source
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)
source
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)
source
@[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) :
A.definable L sᶜ
source
@[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)
source
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)
source
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)
source
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.

source
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 : α ↪ β) [finite β] :
A.definable L ((λ (g : β → M), g ∘ ⇑f) '' s)

Shows that definability is closed under finite projections.

source
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 : α → β) [finite α] [finite β] :
A.definable L ((λ (g : β → M), g ∘ f) '' s)

Shows that definability is closed under finite projections.

source
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
source
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
source
def first_order.language.definable_set (L : first_order.language) {M : Type w} [L.Structure M] (A : set M) (α : Type u_1) :
Type (max u_1 w)

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

Equations
Instances for first_order.language.definable_set
source
@[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
source
@[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} :
has_top (L.definable_set A α)
Equations
source
@[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} :
has_bot (L.definable_set A α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.has_sup {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
has_sup (L.definable_set A α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.has_inf {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
has_inf (L.definable_set A α)
Equations
source
@[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} :
has_compl (L.definable_set A α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.has_sdiff {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
has_sdiff (L.definable_set A α)
Equations
source
@[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} :
inhabited (L.definable_set A α)
Equations
source
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
source
@[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} :
x ∈ ⊤
source
@[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} :
x ∉ ⊥
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem first_order.language.definable_set.mem_sdiff {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
source
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_top {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
↑⊤ = set.univ
source
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_bot {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
↑⊥ = ∅
source
@[simp, norm_cast]
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
source
@[simp, norm_cast]
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
source
@[simp, norm_cast]
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 α) :
↑sᶜ = (↑s)ᶜ
source
@[simp, norm_cast]
theorem first_order.language.definable_set.coe_sdiff {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
source
@[protected, instance]
def first_order.language.definable_set.boolean_algebra {L : first_order.language} {M : Type w} [L.Structure M] {A : set M} {α : Type u_1} :
boolean_algebra (L.definable_set A α)
Equations