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 thatA.Definable L s
indicates that the sets
of a finite cartesian power ofM
is definable with parameters inA
.Set.Definable₁
is defined so thatA.Definable₁ L s
indicates that(s : Set M)
is definable with parameters inA
.Set.Definable₂
is defined so thatA.Definable₂ L s
indicates that(s : Set (M × M))
is definable with parameters inA
.- A
FirstOrder.Language.DefinableSet
is defined so thatL.DefinableSet A α
is the boolean algebra of subsets ofα → M
defined by formulas with parameters inA
.
Main Results #
L.DefinableSet A α
forms aBooleanAlgebra
Set.Definable.image_comp
shows that definability is closed under projections in finite dimensions.
def
Set.Definable
{M : Type w}
(A : Set M)
(L : FirstOrder.Language)
[FirstOrder.Language.Structure L 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}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{s : Set (α → M)}
{L' : FirstOrder.Language}
[FirstOrder.Language.Structure L' M]
(h : Set.Definable A L s)
(φ : L →ᴸ L')
[FirstOrder.Language.LHom.IsExpansionOn φ M]
:
Set.Definable A L' s
theorem
Set.definable_iff_exists_formula_sum
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{s : Set (α → M)}
:
Set.Definable A L s ↔ ∃ φ, s = {v | FirstOrder.Language.Formula.Realize φ (Sum.elim Subtype.val v)}
theorem
Set.empty_definable_iff
{M : Type w}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{s : Set (α → M)}
:
Set.Definable ∅ L s ↔ ∃ φ, s = setOf (FirstOrder.Language.Formula.Realize φ)
theorem
Set.definable_iff_empty_definable_with_params
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{s : Set (α → M)}
:
Set.Definable A L s ↔ Set.Definable ∅ (FirstOrder.Language.withConstants L ↑A) s
theorem
Set.Definable.mono
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{B : Set M}
{s : Set (α → M)}
(hAs : Set.Definable A L s)
(hAB : A ⊆ B)
:
Set.Definable B L s
@[simp]
theorem
Set.definable_empty
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
:
Set.Definable A L ∅
@[simp]
theorem
Set.definable_univ
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
:
Set.Definable A L Set.univ
@[simp]
theorem
Set.Definable.inter
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{f : Set (α → M)}
{g : Set (α → M)}
(hf : Set.Definable A L f)
(hg : Set.Definable A L g)
:
Set.Definable A L (f ∩ g)
@[simp]
theorem
Set.Definable.union
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{f : Set (α → M)}
{g : Set (α → M)}
(hf : Set.Definable A L f)
(hg : Set.Definable A L g)
:
Set.Definable A L (f ∪ g)
theorem
Set.definable_finset_inf
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{ι : Type u_2}
{f : ι → Set (α → M)}
(hf : ∀ (i : ι), Set.Definable A L (f i))
(s : Finset ι)
:
Set.Definable A L (Finset.inf s f)
theorem
Set.definable_finset_sup
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{ι : Type u_2}
{f : ι → Set (α → M)}
(hf : ∀ (i : ι), Set.Definable A L (f i))
(s : Finset ι)
:
Set.Definable A L (Finset.sup s f)
theorem
Set.definable_finset_biInter
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{ι : Type u_2}
{f : ι → Set (α → M)}
(hf : ∀ (i : ι), Set.Definable A L (f i))
(s : Finset ι)
:
Set.Definable A L (⋂ (i : ι) (_ : i ∈ s), f i)
theorem
Set.definable_finset_biUnion
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{ι : Type u_2}
{f : ι → Set (α → M)}
(hf : ∀ (i : ι), Set.Definable A L (f i))
(s : Finset ι)
:
Set.Definable A L (⋃ (i : ι) (_ : i ∈ s), f i)
@[simp]
theorem
Set.Definable.compl
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{s : Set (α → M)}
(hf : Set.Definable A L s)
:
Set.Definable A L sᶜ
@[simp]
theorem
Set.Definable.sdiff
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{s : Set (α → M)}
{t : Set (α → M)}
(hs : Set.Definable A L s)
(ht : Set.Definable A L t)
:
Set.Definable A L (s \ t)
theorem
Set.Definable.preimage_comp
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{β : Type u_1}
(f : α → β)
{s : Set (α → M)}
(h : Set.Definable A L s)
:
Set.Definable A L ((fun g => g ∘ f) ⁻¹' s)
theorem
Set.Definable.image_comp_equiv
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{β : Type u_1}
{s : Set (β → M)}
(h : Set.Definable A L s)
(f : α ≃ β)
:
Set.Definable A L ((fun g => g ∘ ↑f) '' s)
theorem
Set.definable_iff_finitely_definable
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{s : Set (α → M)}
:
Set.Definable A L s ↔ ∃ A0, ↑A0 ⊆ A ∧ Set.Definable (↑A0) L s
theorem
Set.Definable.image_comp_sum_inl_fin
{M : Type w}
{A : Set M}
{L : FirstOrder.Language}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
(m : ℕ)
{s : Set (α ⊕ Fin m → M)}
(h : Set.Definable A L s)
:
Set.Definable A L ((fun g => 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}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{β : Type u_1}
{s : Set (β → M)}
(h : Set.Definable A L s)
(f : α ↪ β)
[Finite β]
:
Set.Definable A L ((fun g => 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}
[FirstOrder.Language.Structure L M]
{α : Type u₁}
{β : Type u_1}
{s : Set (β → M)}
(h : Set.Definable A L s)
(f : α → β)
[Finite α]
[Finite β]
:
Set.Definable A L ((fun g => g ∘ f) '' s)
Shows that definability is closed under finite projections.
def
Set.Definable₁
{M : Type w}
(A : Set M)
(L : FirstOrder.Language)
[FirstOrder.Language.Structure L M]
(s : Set M)
:
A 1-dimensional version of Definable
, for Set M
.
Instances For
def
Set.Definable₂
{M : Type w}
(A : Set M)
(L : FirstOrder.Language)
[FirstOrder.Language.Structure L M]
(s : Set (M × M))
:
A 2-dimensional version of Definable
, for Set (M × M)
.
Instances For
def
FirstOrder.Language.DefinableSet
(L : FirstOrder.Language)
{M : Type w}
[FirstOrder.Language.Structure L 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.
Instances For
instance
FirstOrder.Language.DefinableSet.instSetLike
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
SetLike (FirstOrder.Language.DefinableSet L A α) (α → M)
instance
FirstOrder.Language.DefinableSet.instTop
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
Top (FirstOrder.Language.DefinableSet L A α)
instance
FirstOrder.Language.DefinableSet.instBot
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
Bot (FirstOrder.Language.DefinableSet L A α)
instance
FirstOrder.Language.DefinableSet.instSup
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
Sup (FirstOrder.Language.DefinableSet L A α)
instance
FirstOrder.Language.DefinableSet.instInf
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
Inf (FirstOrder.Language.DefinableSet L A α)
instance
FirstOrder.Language.DefinableSet.instHasCompl
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
instance
FirstOrder.Language.DefinableSet.instSDiff
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
instance
FirstOrder.Language.DefinableSet.instInhabited
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
theorem
FirstOrder.Language.DefinableSet.le_iff
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
{s : FirstOrder.Language.DefinableSet L A α}
{t : FirstOrder.Language.DefinableSet L A α}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.mem_top
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
{x : α → M}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.not_mem_bot
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
{x : α → M}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.mem_sup
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
{s : FirstOrder.Language.DefinableSet L A α}
{t : FirstOrder.Language.DefinableSet L A α}
{x : α → M}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.mem_inf
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
{s : FirstOrder.Language.DefinableSet L A α}
{t : FirstOrder.Language.DefinableSet L A α}
{x : α → M}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.mem_compl
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
{s : FirstOrder.Language.DefinableSet L A α}
{x : α → M}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.mem_sdiff
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
{s : FirstOrder.Language.DefinableSet L A α}
{t : FirstOrder.Language.DefinableSet L A α}
{x : α → M}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_top
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_bot
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_sup
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
(s : FirstOrder.Language.DefinableSet L A α)
(t : FirstOrder.Language.DefinableSet L A α)
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_inf
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
(s : FirstOrder.Language.DefinableSet L A α)
(t : FirstOrder.Language.DefinableSet L A α)
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_compl
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
(s : FirstOrder.Language.DefinableSet L A α)
:
@[simp]
theorem
FirstOrder.Language.DefinableSet.coe_sdiff
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
(s : FirstOrder.Language.DefinableSet L A α)
(t : FirstOrder.Language.DefinableSet L A α)
:
instance
FirstOrder.Language.DefinableSet.instBooleanAlgebra
{L : FirstOrder.Language}
{M : Type w}
[FirstOrder.Language.Structure L M]
{A : Set M}
{α : Type u₁}
: