Documentation

Mathlib.ModelTheory.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 : 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.

Equations
  • A.Definable L s = ∃ (φ : (L.withConstants A).Formula α), s = setOf φ.Realize
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_exists_formula_sum {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (αM)} :
    A.Definable L s ∃ (φ : L.Formula (A α)), s = {v : αM | φ.Realize (Sum.elim Subtype.val v)}
    theorem Set.empty_definable_iff {M : Type w} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (αM)} :
    .Definable L s ∃ (φ : L.Formula α), s = setOf φ.Realize
    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)} :
    A.Definable L s .Definable (L.withConstants A) s
    theorem Set.Definable.mono {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {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 : FirstOrder.Language} [L.Structure M] {α : Type u₁} :
    A.Definable L
    @[simp]
    theorem Set.definable_univ {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} :
    A.Definable L Set.univ
    @[simp]
    theorem Set.Definable.inter {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {f : Set (αM)} {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 : FirstOrder.Language} [L.Structure M] {α : Type u₁} {f : Set (αM)} {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 : 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 (s.inf f)
    theorem Set.definable_finset_sup {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 (s.sup f)
    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 (⋂ is, f i)
    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 (⋃ is, f i)
    @[simp]
    theorem Set.Definable.compl {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (αM)} (hf : A.Definable L s) :
    A.Definable L s
    @[simp]
    theorem Set.Definable.sdiff {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (αM)} {t : Set (αM)} (hs : A.Definable L s) (ht : A.Definable L t) :
    A.Definable L (s \ t)
    @[simp]
    theorem Set.Definable.himp {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (αM)} {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 : FirstOrder.Language} [L.Structure M] {α : Type u₁} {β : Type u_1} (f : αβ) {s : Set (αM)} (h : A.Definable L s) :
    A.Definable L ((fun (g : βM) => g f) ⁻¹' s)
    theorem Set.Definable.image_comp_equiv {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {β : Type u_1} {s : Set (βM)} (h : A.Definable L s) (f : α β) :
    A.Definable L ((fun (g : βM) => g f) '' s)
    theorem Set.definable_iff_finitely_definable {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} {s : Set (αM)} :
    A.Definable L s ∃ (A0 : Finset M), A0 A (↑A0).Definable L s
    theorem Set.Definable.image_comp_sum_inl_fin {M : Type w} {A : Set M} {L : FirstOrder.Language} [L.Structure M] {α : Type u₁} (m : ) {s : Set (α Fin mM)} (h : A.Definable L s) :
    A.Definable L ((fun (g : α Fin mM) => 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} [L.Structure M] {α : Type u₁} {β : Type u_1} {s : Set (βM)} (h : A.Definable L s) (f : α β) [Finite β] :
    A.Definable L ((fun (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 : FirstOrder.Language} [L.Structure M] {α : Type u₁} {β : Type u_1} {s : Set (βM)} (h : A.Definable L s) (f : αβ) [Finite α] [Finite β] :
    A.Definable L ((fun (g : βM) => g f) '' s)

    Shows that definability is closed under finite projections.

    def Set.Definable₁ {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M] (s : Set M) :

    A 1-dimensional version of Definable, for Set M.

    Equations
    • A.Definable₁ L s = A.Definable L {x : Fin 1M | x 0 s}
    Instances For
      def Set.Definable₂ {M : Type w} (A : Set M) (L : FirstOrder.Language) [L.Structure M] (s : Set (M × M)) :

      A 2-dimensional version of Definable, for Set (M × M).

      Equations
      • A.Definable₂ L s = A.Definable L {x : Fin 2M | (x 0, x 1) s}
      Instances For
        def FirstOrder.Language.DefinableSet (L : FirstOrder.Language) {M : Type w} [L.Structure 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.

        Equations
        • L.DefinableSet A α = { s : Set (αM) // A.Definable L s }
        Instances For
          instance FirstOrder.Language.DefinableSet.instSetLike {L : FirstOrder.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.instTop {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          Top (L.DefinableSet A α)
          Equations
          • FirstOrder.Language.DefinableSet.instTop = { top := , }
          instance FirstOrder.Language.DefinableSet.instBot {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          Bot (L.DefinableSet A α)
          Equations
          • FirstOrder.Language.DefinableSet.instBot = { bot := , }
          instance FirstOrder.Language.DefinableSet.instSup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          Sup (L.DefinableSet A α)
          Equations
          • FirstOrder.Language.DefinableSet.instSup = { sup := fun (s t : L.DefinableSet A α) => s t, }
          instance FirstOrder.Language.DefinableSet.instInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          Inf (L.DefinableSet A α)
          Equations
          • FirstOrder.Language.DefinableSet.instInf = { inf := fun (s t : L.DefinableSet A α) => s t, }
          instance FirstOrder.Language.DefinableSet.instHasCompl {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          HasCompl (L.DefinableSet A α)
          Equations
          • FirstOrder.Language.DefinableSet.instHasCompl = { compl := fun (s : L.DefinableSet A α) => (↑s), }
          instance FirstOrder.Language.DefinableSet.instSDiff {L : FirstOrder.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 : FirstOrder.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 : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          Inhabited (L.DefinableSet A α)
          Equations
          • FirstOrder.Language.DefinableSet.instInhabited = { default := }
          theorem FirstOrder.Language.DefinableSet.le_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s : L.DefinableSet A α} {t : L.DefinableSet A α} :
          s t s t
          @[simp]
          theorem FirstOrder.Language.DefinableSet.mem_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {x : αM} :
          @[simp]
          theorem FirstOrder.Language.DefinableSet.not_mem_bot {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {x : αM} :
          x
          @[simp]
          theorem FirstOrder.Language.DefinableSet.mem_sup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s : L.DefinableSet A α} {t : L.DefinableSet A α} {x : αM} :
          x s t x s x t
          @[simp]
          theorem FirstOrder.Language.DefinableSet.mem_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s : L.DefinableSet A α} {t : L.DefinableSet A α} {x : αM} :
          x s t x s x t
          @[simp]
          theorem FirstOrder.Language.DefinableSet.mem_compl {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s : L.DefinableSet A α} {x : αM} :
          x s xs
          @[simp]
          theorem FirstOrder.Language.DefinableSet.mem_sdiff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} {s : L.DefinableSet A α} {t : L.DefinableSet A α} {x : αM} :
          x s \ t x s xt
          @[simp]
          theorem FirstOrder.Language.DefinableSet.coe_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          = Set.univ
          @[simp]
          theorem FirstOrder.Language.DefinableSet.coe_bot {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          =
          @[simp]
          theorem FirstOrder.Language.DefinableSet.coe_sup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s : L.DefinableSet A α) (t : L.DefinableSet A α) :
          (s t) = s t
          @[simp]
          theorem FirstOrder.Language.DefinableSet.coe_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s : L.DefinableSet A α) (t : L.DefinableSet A α) :
          (s t) = s t
          @[simp]
          theorem FirstOrder.Language.DefinableSet.coe_compl {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s : L.DefinableSet A α) :
          s = (↑s)
          @[simp]
          theorem FirstOrder.Language.DefinableSet.coe_sdiff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s : L.DefinableSet A α) (t : L.DefinableSet A α) :
          (s \ t) = s \ t
          @[simp]
          theorem FirstOrder.Language.DefinableSet.coe_himp {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} (s : L.DefinableSet A α) (t : L.DefinableSet A α) :
          (s t) = s t
          noncomputable instance FirstOrder.Language.DefinableSet.instBooleanAlgebra {L : FirstOrder.Language} {M : Type w} [L.Structure M] {A : Set M} {α : Type u₁} :
          BooleanAlgebra (L.DefinableSet A α)
          Equations