Relations and functions defined by a first-order formula (with parameter)

@[reducible, inline]

abbrev FFL.FirstOrder.IsDefinedBy {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} (R : (Fin k → M) → Prop) (φ : Semisentence L k) : Prop

Equations

• FFL.FirstOrder.IsDefinedBy R φ = ∀ (v : Fin k → M), (FFL.FirstOrder.Semiformula.Evalb v) φ ↔ R v

class FFL.FirstOrder.Defined {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} (R : outParam ((Fin k → M) → Prop)) (φ : Semisentence L k) : Prop

• iff : IsDefinedBy R φ

@[reducible, inline]

abbrev FFL.FirstOrder.IsDefinedByWithParam {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} (R : (Fin k → M) → Prop) (φ : Semiformula L M k) : Prop

The relation R is definable by a formula φ with parameters over the domain M. Here, the free variables of φ are indexed by the type M, so that φ may contain finitely many parameters, which are interpreted by using id : M → M for the valuation of free variables.

Equations

• FFL.FirstOrder.IsDefinedByWithParam R φ = ∀ (v : Fin k → M), (FFL.FirstOrder.Semiformula.Eval v id) φ ↔ R v

@[simp]

theorem FFL.FirstOrder.Defined.eval_iff {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} {R : (Fin k → M) → Prop} {φ : Semisentence L k} [h : Defined R φ] (v : Fin k → M) : (Semiformula.Evalb v) φ ↔ R v

theorem FFL.FirstOrder.IsDefinedByWithParam.iff {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} {R : (Fin k → M) → Prop} {φ : Semiformula L M k} (h : IsDefinedByWithParam R φ) (v : Fin k → M) : (Semiformula.Eval v id) φ ↔ R v

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedFunction {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} (f : (Fin k → M) → M) (φ : Semisentence L (k + 1)) : Prop

Equations

• FFL.FirstOrder.DefinedFunction f φ = FFL.FirstOrder.Defined (fun (v : Fin (k + 1) → M) => v 0 = f fun (x : Fin k) => v x.succ) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedPred {L : Language} {M : Type u_1} [Tarski.Structure L M] (P : M → Prop) (φ : Semisentence L 1) : Prop

Equations

• FFL.FirstOrder.DefinedPred P φ = FFL.FirstOrder.Defined (fun (v : Fin 1 → M) => P (v 0)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedRel {L : Language} {M : Type u_1} [Tarski.Structure L M] (R : M → M → Prop) (φ : Semisentence L 2) : Prop

Equations

• FFL.FirstOrder.DefinedRel R φ = FFL.FirstOrder.Defined (fun (v : Fin 2 → M) => R (v 0) (v 1)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedRel₃ {L : Language} {M : Type u_1} [Tarski.Structure L M] (R : M → M → M → Prop) (φ : Semisentence L 3) : Prop

Equations

• FFL.FirstOrder.DefinedRel₃ R φ = FFL.FirstOrder.Defined (fun (v : Fin 3 → M) => R (v 0) (v 1) (v 2)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedRel₄ {L : Language} {M : Type u_1} [Tarski.Structure L M] (R : M → M → M → M → Prop) (φ : Semisentence L 4) : Prop

Equations

• FFL.FirstOrder.DefinedRel₄ R φ = FFL.FirstOrder.Defined (fun (v : Fin 4 → M) => R (v 0) (v 1) (v 2) (v 3)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedFunction₀ {L : Language} {M : Type u_1} [Tarski.Structure L M] (c : M) (φ : Semisentence L 1) : Prop

Equations

• FFL.FirstOrder.DefinedFunction₀ c φ = FFL.FirstOrder.DefinedFunction (fun (x : Fin 0 → M) => c) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedFunction₁ {L : Language} {M : Type u_1} [Tarski.Structure L M] (f : M → M) (φ : Semisentence L 2) : Prop

Equations

• FFL.FirstOrder.DefinedFunction₁ f φ = FFL.FirstOrder.DefinedFunction (fun (v : Fin 1 → M) => f (v 0)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedFunction₂ {L : Language} {M : Type u_1} [Tarski.Structure L M] (f : M → M → M) (φ : Semisentence L 3) : Prop

Equations

• FFL.FirstOrder.DefinedFunction₂ f φ = FFL.FirstOrder.DefinedFunction (fun (v : Fin 2 → M) => f (v 0) (v 1)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedFunction₃ {L : Language} {M : Type u_1} [Tarski.Structure L M] (f : M → M → M → M) (φ : Semisentence L 4) : Prop

Equations

• FFL.FirstOrder.DefinedFunction₃ f φ = FFL.FirstOrder.DefinedFunction (fun (v : Fin 3 → M) => f (v 0) (v 1) (v 2)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedFunction₄ {L : Language} {M : Type u_1} [Tarski.Structure L M] (f : M → M → M → M → M) (φ : Semisentence L 5) : Prop

Equations

• FFL.FirstOrder.DefinedFunction₄ f φ = FFL.FirstOrder.DefinedFunction (fun (v : Fin 4 → M) => f (v 0) (v 1) (v 2) (v 3)) φ

@[reducible, inline]

abbrev FFL.FirstOrder.DefinedFunction₅ {L : Language} {M : Type u_1} [Tarski.Structure L M] (f : M → M → M → M → M → M) (φ : Semisentence L 6) : Prop

Equations

• FFL.FirstOrder.DefinedFunction₅ f φ = FFL.FirstOrder.DefinedFunction (fun (v : Fin 5 → M) => f (v 0) (v 1) (v 2) (v 3) (v 4)) φ

def FFL.FirstOrder.«term_-relation_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-relation₃_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-relation₄_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₀_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₁_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₂_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₃_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₄_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₅_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-predicate[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-relation[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-relation₃[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-relation₄[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₀[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₁[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₂[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₃[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₄[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.«term_-function₅[_]_Via_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

class FFL.FirstOrder.Language.Definable (L : Language) {M : Type u_1} [Tarski.Structure L M] {k : ℕ} (P : (Fin k → M) → Prop) : Prop

• definable : ∃ (φ : Semiformula L M k), IsDefinedByWithParam P φ

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinablePred (L : Language) {M : Type u_1} [Tarski.Structure L M] (P : M → Prop) : Prop

Equations

• (L-predicate P) = L.Definable fun (v : Fin 1 → M) => P (v 0)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableRel (L : Language) {M : Type u_1} [Tarski.Structure L M] (P : M → M → Prop) : Prop

Equations

• (L-relation P) = L.Definable fun (v : Fin 2 → M) => P (v 0) (v 1)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableRel₃ (L : Language) {M : Type u_1} [Tarski.Structure L M] (P : M → M → M → Prop) : Prop

Equations

• (L-relation₃ P) = L.Definable fun (v : Fin 3 → M) => P (v 0) (v 1) (v 2)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableRel₄ (L : Language) {M : Type u_1} [Tarski.Structure L M] (P : M → M → M → M → Prop) : Prop

Equations

• (L-relation₄ P) = L.Definable fun (v : Fin 4 → M) => P (v 0) (v 1) (v 2) (v 3)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableRel₅ (L : Language) {M : Type u_1} [Tarski.Structure L M] (P : M → M → M → M → M → Prop) : Prop

Equations

• (L-relation₅ P) = L.Definable fun (v : Fin 5 → M) => P (v 0) (v 1) (v 2) (v 3) (v 4)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableRel₆ (L : Language) {M : Type u_1} [Tarski.Structure L M] (P : M → M → M → M → M → M → Prop) : Prop

Equations

• L.DefinableRel₆ P = L.Definable fun (v : Fin 6 → M) => P (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableFunction (L : Language) {M : Type u_1} [Tarski.Structure L M] {k : ℕ} (f : (Fin k → M) → M) : Prop

Equations

• L.DefinableFunction f = L.Definable fun (v : Fin (k + 1) → M) => v 0 = f fun (x : Fin k) => v x.succ

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableFunction₀ (L : Language) {M : Type u_1} [Tarski.Structure L M] (c : M) : Prop

Equations

• L.DefinableFunction₀ c = L.DefinableFunction fun (x : Fin 0 → M) => c

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableFunction₁ (L : Language) {M : Type u_1} [Tarski.Structure L M] (f : M → M) : Prop

Equations

• (L-function₁ f) = L.DefinableFunction fun (v : Fin 1 → M) => f (v 0)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableFunction₂ (L : Language) {M : Type u_1} [Tarski.Structure L M] (f : M → M → M) : Prop

Equations

• (L-function₂ f) = L.DefinableFunction fun (v : Fin 2 → M) => f (v 0) (v 1)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableFunction₃ (L : Language) {M : Type u_1} [Tarski.Structure L M] (f : M → M → M → M) : Prop

Equations

• (L-function₃ f) = L.DefinableFunction fun (v : Fin 3 → M) => f (v 0) (v 1) (v 2)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableFunction₄ (L : Language) {M : Type u_1} [Tarski.Structure L M] (f : M → M → M → M → M) : Prop

Equations

• (L-function₄ f) = L.DefinableFunction fun (v : Fin 4 → M) => f (v 0) (v 1) (v 2) (v 3)

@[reducible, inline]

abbrev FFL.FirstOrder.Language.DefinableFunction₅ (L : Language) {M : Type u_1} [Tarski.Structure L M] (f : M → M → M → M → M → M) : Prop

Equations

• L.DefinableFunction₅ f = L.DefinableFunction fun (v : Fin 5 → M) => f (v 0) (v 1) (v 2) (v 3) (v 4)

def FFL.FirstOrder.Language.«term_-predicate_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation₃_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation₄_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation₅_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₁_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₂_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₃_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₄_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-predicate[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation₃[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation₄[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-relation₅[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₁[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₂[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₃[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.«term_-function₄[_]_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem FFL.FirstOrder.IsDefinedBy.of_vec_one {L : Language} {M : Type u_1} [Tarski.Structure L M] {R : (Fin 1 → M) → Prop} {φ : Semisentence L 1} (h : ∀ (x : M), (Semiformula.Evalb ![x]) φ ↔ R ![x]) : IsDefinedBy R φ

theorem FFL.FirstOrder.IsDefinedBy.of_vec_two {L : Language} {M : Type u_1} [Tarski.Structure L M] {R : (Fin 2 → M) → Prop} {φ : Semisentence L 2} (h : ∀ (x y : M), (Semiformula.Evalb ![x, y]) φ ↔ R ![x, y]) : IsDefinedBy R φ

theorem FFL.FirstOrder.IsDefinedBy.of_vec_three {L : Language} {M : Type u_1} [Tarski.Structure L M] {R : (Fin 3 → M) → Prop} {φ : Semisentence L 3} (h : ∀ (x y z : M), (Semiformula.Evalb ![x, y, z]) φ ↔ R ![x, y, z]) : IsDefinedBy R φ

theorem FFL.FirstOrder.Defined.to_definable {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} {R : (Fin k → M) → Prop} {φ : Semisentence L k} (hR : Defined R φ) : L.Definable R

theorem FFL.FirstOrder.DefinedFunction.to_definable {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} {f : (Fin k → M) → M} {φ : Semisentence L (k + 1)} (hf : DefinedFunction f φ) : L.DefinableFunction f

theorem FFL.FirstOrder.Language.Definable.of_iff {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {P Q : (Fin k → M) → Prop} (H : L.Definable Q) (h : ∀ (x : Fin k → M), P x ↔ Q x) : L.Definable P

@[simp]

theorem FFL.FirstOrder.Language.Definable.const {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] (p : Prop) : L.Definable fun (x : Fin k → M) => p

theorem FFL.FirstOrder.Language.Definable.and {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {R S : (Fin k → M) → Prop} (hR : L.Definable R) (hS : L.Definable S) : L.Definable fun (v : Fin k → M) => R v ∧ S v

theorem FFL.FirstOrder.Language.Definable.or {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {R S : (Fin k → M) → Prop} (hR : L.Definable R) (hS : L.Definable S) : L.Definable fun (v : Fin k → M) => R v ∨ S v

theorem FFL.FirstOrder.Language.Definable.imp {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {R S : (Fin k → M) → Prop} (hR : L.Definable R) (hS : L.Definable S) : L.Definable fun (v : Fin k → M) => R v → S v

theorem FFL.FirstOrder.Language.Definable.not {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {R : (Fin k → M) → Prop} (hR : L.Definable R) : L.Definable fun (v : Fin k → M) => ¬R v

theorem FFL.FirstOrder.Language.Definable.biconditional {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {R S : (Fin k → M) → Prop} (hR : L.Definable R) (hS : L.Definable S) : L.Definable fun (v : Fin k → M) => R v ↔ S v

theorem FFL.FirstOrder.Language.Definable.all {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {R : (Fin k → M) → M → Prop} (hR : L.Definable fun (w : Fin (k + 1) → M) => R (fun (x : Fin k) => w x.succ) (w 0)) : L.Definable fun (v : Fin k → M) => ∀ (x : M), R v x

theorem FFL.FirstOrder.Language.Definable.exs {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {R : (Fin k → M) → M → Prop} (hR : L.Definable fun (w : Fin (k + 1) → M) => R (fun (x : Fin k) => w x.succ) (w 0)) : L.Definable fun (v : Fin k → M) => ∃ (x : M), R v x

instance FFL.FirstOrder.Language.Definable.eq {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] : L-relation Eq

instance FFL.FirstOrder.Language.Definable.lt {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.LT] [LT M] [Tarski.Structure.LT L M] : L-relation _root_.LT.lt

instance FFL.FirstOrder.Language.Definable.mem {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Mem] [Membership M M] [Tarski.Structure.Mem L M] : L-relation Membership.mem

theorem FFL.FirstOrder.Language.Definable.fconj {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {ι : Type u_2} {P : ι → (Fin k → M) → Prop} (s : Finset ι) (h : ∀ (i : ι), L.Definable fun (w : Fin k → M) => P i w) : L.Definable fun (v : Fin k → M) => ∀ i ∈ s, P i v

theorem FFL.FirstOrder.Language.Definable.fdisj {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {ι : Type u_2} {P : ι → (Fin k → M) → Prop} (s : Finset ι) (h : ∀ (i : ι), L.Definable fun (w : Fin k → M) => P i w) : L.Definable fun (v : Fin k → M) => ∃ i ∈ s, P i v

theorem FFL.FirstOrder.Language.Definable.fintype_all {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {ι : Type u_2} [Fintype ι] {P : ι → (Fin k → M) → Prop} (h : ∀ (i : ι), L.Definable fun (w : Fin k → M) => P i w) : L.Definable fun (v : Fin k → M) => ∀ (i : ι), P i v

theorem FFL.FirstOrder.Language.Definable.fintype_exs {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {ι : Type u_2} [Fintype ι] {P : ι → (Fin k → M) → Prop} (h : ∀ (i : ι), L.Definable fun (w : Fin k → M) => P i w) : L.Definable fun (v : Fin k → M) => ∃ (i : ι), P i v

theorem FFL.FirstOrder.Language.Definable.retraction {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {P : (Fin k → M) → Prop} (h : L.Definable P) {n : ℕ} (f : Fin k → Fin n) : L.Definable fun (v : Fin n → M) => P fun (i : Fin k) => v (f i)

theorem FFL.FirstOrder.Language.Definable.exsVec {L : Language} {M : Type u_1} [Tarski.Structure L M] {k l : ℕ} {P : (Fin k → M) → (Fin l → M) → Prop} (h : L.Definable fun (w : Fin (k + l) → M) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) : L.Definable fun (v : Fin k → M) => ∃ (ys : Fin l → M), P v ys

theorem FFL.FirstOrder.Language.Definable.allVec {L : Language} {M : Type u_1} [Tarski.Structure L M] {k l : ℕ} {P : (Fin k → M) → (Fin l → M) → Prop} (h : L.Definable fun (w : Fin (k + l) → M) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j)) : L.Definable fun (v : Fin k → M) => ∀ (ys : Fin l → M), P v ys

theorem FFL.FirstOrder.Language.Definable.substitution {k : ℕ} {L : Language} {M : Type u_1} [Tarski.Structure L M] {l : ℕ} {P : (Fin k → M) → Prop} {f : Fin k → (Fin l → M) → M} (hP : L.Definable P) (hf : ∀ (i : Fin k), L.DefinableFunction (f i)) : L.Definable fun (z : Fin l → M) => P fun (x : Fin k) => f x z

theorem FFL.FirstOrder.Language.DefinablePred.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] {P : M → Prop} {k : ℕ} {f : (Fin k → M) → M} [hP : L-predicate P] (hf : L.DefinableFunction f) : L.Definable fun (v : Fin k → M) => P (f v)

theorem FFL.FirstOrder.Language.DefinableRel.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] {P : M → M → Prop} {k : ℕ} {f g : (Fin k → M) → M} [hP : L-relation P] (hf : L.DefinableFunction f) (hg : L.DefinableFunction g) : L.Definable fun (v : Fin k → M) => P (f v) (g v)

theorem FFL.FirstOrder.Language.DefinableRel₃.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} {P : M → M → M → Prop} {f₁ f₂ f₃ : (Fin k → M) → M} [hP : L-relation₃ P] (hf₁ : L.DefinableFunction f₁) (hf₂ : L.DefinableFunction f₂) (hf₃ : L.DefinableFunction f₃) : L.Definable fun (v : Fin k → M) => P (f₁ v) (f₂ v) (f₃ v)

theorem FFL.FirstOrder.Language.DefinableRel₄.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} {P : M → M → M → M → Prop} {f₁ f₂ f₃ f₄ : (Fin k → M) → M} [hP : L-relation₄ P] (hf₁ : L.DefinableFunction f₁) (hf₂ : L.DefinableFunction f₂) (hf₃ : L.DefinableFunction f₃) (hf₄ : L.DefinableFunction f₄) : L.Definable fun (v : Fin k → M) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v)

theorem FFL.FirstOrder.Language.DefinableRel₅.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] {k : ℕ} {P : M → M → M → M → M → Prop} {f₁ f₂ f₃ f₄ f₅ : (Fin k → M) → M} [hP : L-relation₅ P] (hf₁ : L.DefinableFunction f₁) (hf₂ : L.DefinableFunction f₂) (hf₃ : L.DefinableFunction f₃) (hf₄ : L.DefinableFunction f₄) (hf₅ : L.DefinableFunction f₅) : L.Definable fun (v : Fin k → M) => P (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

theorem FFL.FirstOrder.Language.DefinablePred.of_iff {L : Language} {M : Type u_1} [Tarski.Structure L M] {P Q : M → Prop} (H : L-predicate Q) (h : ∀ (x : M), P x ↔ Q x) : L-predicate P

instance FFL.FirstOrder.Language.DefinableFunction₁.graph {L : Language} {M : Type u_1} [Tarski.Structure L M] {f : M → M} [h : L-function₁ f] : L-relation Function.Graph f

instance FFL.FirstOrder.Language.DefinableFunction₂.graph {L : Language} {M : Type u_1} [Tarski.Structure L M] {f : M → M → M} [h : L-function₂ f] : L-relation₃ Function.Graph₂ f

instance FFL.FirstOrder.Language.DefinableFunction₃.graph {L : Language} {M : Type u_1} [Tarski.Structure L M] {f : M → M → M → M} [h : L-function₃ f] : L-relation₄ Function.Graph₃ f

Definable functions

instance FFL.FirstOrder.Language.DefinableFunction.projection {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k : ℕ} (i : Fin k) : L.DefinableFunction fun (w : Fin k → M) => w i

instance FFL.FirstOrder.Language.DefinableFunction.const {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k : ℕ} (c : M) : L.DefinableFunction fun (x : Fin k → M) => c

theorem FFL.FirstOrder.Language.DefinableFunction.substitution {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k l : ℕ} {F : (Fin k → M) → M} {f : Fin k → (Fin l → M) → M} (hF : L.DefinableFunction F) (hf : ∀ (i : Fin k), L.DefinableFunction (f i)) : L.DefinableFunction fun (z : Fin l → M) => F fun (i : Fin k) => f i z

instance FFL.FirstOrder.Language.DefinableFunction.hAdd {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] [L.Add] [Add M] [Tarski.Structure.Add L M] : L-function₂ HAdd.hAdd

instance FFL.FirstOrder.Language.DefinableFunction.hMul {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] [L.Mul] [Mul M] [Tarski.Structure.Mul L M] : L-function₂ HMul.hMul

theorem FFL.FirstOrder.Language.DefinableFunction₁.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k : ℕ} {F : M → M} {f : (Fin k → M) → M} [hF : L-function₁ F] (hf : L.DefinableFunction f) : L.DefinableFunction fun (v : Fin k → M) => F (f v)

theorem FFL.FirstOrder.Language.DefinableFunction₂.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k : ℕ} {F : M → M → M} {f₁ f₂ : (Fin k → M) → M} [hF : L-function₂ F] (hf₁ : L.DefinableFunction f₁) (hf₂ : L.DefinableFunction f₂) : L.DefinableFunction fun (v : Fin k → M) => F (f₁ v) (f₂ v)

theorem FFL.FirstOrder.Language.DefinableFunction₃.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k : ℕ} {F : M → M → M → M} {f₁ f₂ f₃ : (Fin k → M) → M} [hF : L-function₃ F] (hf₁ : L.DefinableFunction f₁) (hf₂ : L.DefinableFunction f₂) (hf₃ : L.DefinableFunction f₃) : L.DefinableFunction fun (v : Fin k → M) => F (f₁ v) (f₂ v) (f₃ v)

theorem FFL.FirstOrder.Language.DefinableFunction₄.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k : ℕ} {F : M → M → M → M → M} {f₁ f₂ f₃ f₄ : (Fin k → M) → M} [hF : L-function₄ F] (hf₁ : L.DefinableFunction f₁) (hf₂ : L.DefinableFunction f₂) (hf₃ : L.DefinableFunction f₃) (hf₄ : L.DefinableFunction f₄) : L.DefinableFunction fun (v : Fin k → M) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v)

theorem FFL.FirstOrder.Language.DefinableFunction₅.comp {L : Language} {M : Type u_1} [Tarski.Structure L M] [L.Eq] [Tarski.Structure.Eq L M] {k : ℕ} {F : M → M → M → M → M → M} {f₁ f₂ f₃ f₄ f₅ : (Fin k → M) → M} [hF : L.DefinableFunction₅ F] (hf₁ : L.DefinableFunction f₁) (hf₂ : L.DefinableFunction f₂) (hf₃ : L.DefinableFunction f₃) (hf₄ : L.DefinableFunction f₄) (hf₅ : L.DefinableFunction f₅) : L.DefinableFunction fun (v : Fin k → M) => F (f₁ v) (f₂ v) (f₃ v) (f₄ v) (f₅ v)

def FFL.FirstOrder.Language.attrDefinability : Lean.ParserDescr

Equations

• FFL.FirstOrder.Language.attrDefinability = Lean.ParserDescr.node `FFL.FirstOrder.Language.attrDefinability 1024 (Lean.ParserDescr.nonReservedSymbol "definability" false)

def FFL.FirstOrder.Language.tacticDefinability_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def FFL.FirstOrder.Language.tacticDefinability?_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.