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 #

Definability #

source
structure first_order.language.is_definable (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] (s : set (α → M)) :
Prop

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

source
@[simp]
theorem first_order.language.is_definable_empty {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
L.is_definable ∅
source
@[simp]
theorem first_order.language.is_definable_univ {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
L.is_definable set.univ
source
@[simp]
theorem first_order.language.is_definable.inter {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {f g : set (α → M)} (hf : L.is_definable f) (hg : L.is_definable g) :
L.is_definable (f ∩ g)
source
@[simp]
theorem first_order.language.is_definable.union {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {f g : set (α → M)} (hf : L.is_definable f) (hg : L.is_definable g) :
L.is_definable (f ∪ g)
source
@[simp]
theorem first_order.language.is_definable.compl {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s : set (α → M)} (hf : L.is_definable s) :
L.is_definable sᶜ
source
@[simp]
theorem first_order.language.is_definable.sdiff {L : first_order.language} {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s t : set (α → M)} (hs : L.is_definable s) (ht : L.is_definable t) :
L.is_definable (s \ t)
source
def first_order.language.definable_set (L : first_order.language) (M : Type u_3) [L.Structure M] (α : Type) [fintype α] :
Type u_3

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

Equations
source
@[protected, instance]
def first_order.language.definable_set.has_top (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
has_top (L.definable_set M α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.has_bot (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
has_bot (L.definable_set M α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.inhabited (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
inhabited (L.definable_set M α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.pi.set_like (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
set_like (L.definable_set M α) (α → M)
Equations
source
@[simp]
theorem first_order.language.definable_set.mem_top (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {x : α → M} :
x ∈ ⊤
source
@[simp]
theorem first_order.language.definable_set.coe_top (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
↑⊤ = ⊤
source
@[simp]
theorem first_order.language.definable_set.not_mem_bot (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {x : α → M} :
x ∉ ⊥
source
@[simp]
theorem first_order.language.definable_set.coe_bot (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
↑⊥ = ⊥
source
@[protected, instance]
def first_order.language.definable_set.lattice (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
lattice (L.definable_set M α)
Equations
source
theorem first_order.language.definable_set.le_iff (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s t : L.definable_set M α} :
s ≤ t ↔ ↑s ≤ ↑t
source
@[simp]
theorem first_order.language.definable_set.coe_sup (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s t : L.definable_set M α} :
↑(s ⊔ t) = ↑s ∪ ↑t
source
@[simp]
theorem first_order.language.definable_set.mem_sup (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s t : L.definable_set M α} {x : α → M} :
x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t
source
@[simp]
theorem first_order.language.definable_set.coe_inf (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s t : L.definable_set M α} :
↑(s ⊓ t) = ↑s ∩ ↑t
source
@[simp]
theorem first_order.language.definable_set.mem_inf (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s t : L.definable_set M α} {x : α → M} :
x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t
source
@[protected, instance]
def first_order.language.definable_set.bounded_order (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
bounded_order (L.definable_set M α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.distrib_lattice (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
distrib_lattice (L.definable_set M α)
Equations
source
@[protected, instance]
def first_order.language.definable_set.has_compl (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
has_compl (L.definable_set M α)

The complement of a definable set is also definable.

Equations
source
@[simp]
theorem first_order.language.definable_set.mem_compl (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s : L.definable_set M α} {x : α → M} :
x ∈ sᶜ ↔ x ∉ s
source
@[simp]
theorem first_order.language.definable_set.coe_compl (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] {s : L.definable_set M α} :
↑sᶜ = (↑s)ᶜ
source
@[protected, instance]
def first_order.language.definable_set.boolean_algebra (L : first_order.language) {M : Type u_3} [L.Structure M] {α : Type} [fintype α] :
boolean_algebra (L.definable_set M α)
Equations