Supporting results for pointwise provable equality.

Language of first-order logic

This file defines the language of first-order logic.

• FFL.FirstOrder.Language.empty is the empty language.
• FFL.FirstOrder.Language.ofConstants C is a language with only constants of the element C.
• FFL.FirstOrder.Language.oRing, ℒₒᵣ is the language of ordered ring.

structure PointwiseComposition.FFL.FirstOrder.Language : Type (u + 1)

Function and relation symbols indexed by their arities.

• Func : ℕ → Type u

  The Func construction in FFL.FirstOrder.Language.

• Rel : ℕ → Type u

  The Rel construction in FFL.FirstOrder.Language.

class PointwiseComposition.FFL.FirstOrder.Language.Relational (L : Language) : Prop

Data and laws for Relational in FFL.FirstOrder.Language.

• func_empty (k : ℕ) : IsEmpty (L.Func k)

instance PointwiseComposition.FFL.FirstOrder.Language.instIsEmptyFuncOfRelational {k : ℕ} {L : Language} [L.Relational] : IsEmpty (L.Func k)

class PointwiseComposition.FFL.FirstOrder.Language.IsConstant (L : Language) : Prop

Data and laws for Is Constant in FFL.FirstOrder.Language.

• func_empty (k : ℕ) : IsEmpty (L.Func (k + 1))
• rel_empty (k : ℕ) : IsEmpty (L.Rel k)

class PointwiseComposition.FFL.FirstOrder.Language.ConstantInhabited (L : Language) extends Inhabited (L.Func 0) : Type u_1

Data and laws for Constant Inhabited in FFL.FirstOrder.Language.

• default : L.Func 0

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instInhabitedFuncOfNatNatOfConstantInhabited {L : Language} [L.ConstantInhabited] : Inhabited (L.Func 0)

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instInhabitedFuncOfNatNatOfConstantInhabited = inferInstance

def PointwiseComposition.FFL.FirstOrder.Language.empty : Language

The empty construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.empty = { Func := fun (x : ℕ) => PEmpty.{?u.1 + 1}, Rel := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instInhabited : Inhabited Language

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instInhabited = { default := PointwiseComposition.FFL.FirstOrder.Language.empty }

inductive PointwiseComposition.FFL.FirstOrder.Language.GraphFunc : ℕ → Type

Data and laws for Graph Func in FFL.FirstOrder.Language.

• start : GraphFunc 0
• terminal : GraphFunc 0

inductive PointwiseComposition.FFL.FirstOrder.Language.GraphRel : ℕ → Type

Data and laws for Graph Rel in FFL.FirstOrder.Language.

• equal : GraphRel 2
• le : GraphRel 2

def PointwiseComposition.FFL.FirstOrder.Language.graph : Language

The graph construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.graph = { Func := PointwiseComposition.FFL.FirstOrder.Language.GraphFunc, Rel := PointwiseComposition.FFL.FirstOrder.Language.GraphRel }

inductive PointwiseComposition.FFL.FirstOrder.Language.BinaryRel : ℕ → Type

Data and laws for Binary Rel in FFL.FirstOrder.Language.

• isone : BinaryRel 1
• equal : BinaryRel 2
• le : BinaryRel 2

def PointwiseComposition.FFL.FirstOrder.Language.binary : Language

The binary construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.binary = { Func := fun (x : ℕ) => Empty, Rel := PointwiseComposition.FFL.FirstOrder.Language.BinaryRel }

inductive PointwiseComposition.FFL.FirstOrder.Language.EqRel : ℕ → Type

Data and laws for Eq Rel in FFL.FirstOrder.Language.

• equal : EqRel 2

@[reducible]

def PointwiseComposition.FFL.FirstOrder.Language.equal : Language

The equal construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.equal = { Func := fun (x : ℕ) => Empty, Rel := PointwiseComposition.FFL.FirstOrder.Language.EqRel }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instToStringFuncEqual (k : ℕ) : ToString (equal.Func k)

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instToStringFuncEqual k = { toString := fun (x : PointwiseComposition.FFL.FirstOrder.Language.equal.Func k) => "" }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instToStringRelEqual (k : ℕ) : ToString (equal.Rel k)

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instToStringRelEqual k = { toString := fun (x : PointwiseComposition.FFL.FirstOrder.Language.equal.Rel k) => "\\mathrm{Eq}" }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instDecidableEqFuncEqual (k : ℕ) : DecidableEq (equal.Func k)

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instDecidableEqFuncEqual k a b = Empty.casesOn (fun (x : PointwiseComposition.FFL.FirstOrder.Language.equal.Func k) => Decidable (x = b)) a

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instDecidableEqRelEqual (k : ℕ) : DecidableEq (equal.Rel k)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instEncodableFuncEqual (k : ℕ) : Encodable (equal.Func k)

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instEncodableFuncEqual k = IsEmpty.toEncodable

inductive PointwiseComposition.FFL.FirstOrder.Language.ORing.Func : ℕ → Type

Data and laws for Func in FFL.FirstOrder.Language.ORing.

• zero : Func 0
• one : Func 0
• add : Func 2
• mul : Func 2

inductive PointwiseComposition.FFL.FirstOrder.Language.ORing.Rel : ℕ → Type

Data and laws for Rel in FFL.FirstOrder.Language.ORing.

• eq : Rel 2
• lt : Rel 2

@[reducible]

def PointwiseComposition.FFL.FirstOrder.Language.oRing : Language

The ℒₒᵣ construction in ℒₒᵣ.

Equations

• ℒₒᵣ = { Func := PointwiseComposition.FFL.FirstOrder.Language.ORing.Func, Rel := PointwiseComposition.FFL.FirstOrder.Language.ORing.Rel }

def PointwiseComposition.FFL.FirstOrder.Language.termℒₒᵣ : Lean.ParserDescr

The termℒₒᵣ construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.termℒₒᵣ = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Language.termℒₒᵣ 1024 (Lean.ParserDescr.symbol "ℒₒᵣ")

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.ORing.instToStringFuncORing (k : ℕ) : ToString (ℒₒᵣ.Func k)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.ORing.instToStringRelORing (k : ℕ) : ToString (ℒₒᵣ.Rel k)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.ORing.instDecidableEqFuncORing (k : ℕ) : DecidableEq (ℒₒᵣ.Func k)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.ORing.instDecidableEqRelORing (k : ℕ) : DecidableEq (ℒₒᵣ.Rel k)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.ORing.instEncodableFuncORing (k : ℕ) : Encodable (ℒₒᵣ.Func k)

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Language.ORing.Func1IsEmpty : IsEmpty (ℒₒᵣ.Func 1)

theorem PointwiseComposition.FFL.FirstOrder.Language.ORing.FuncGe3IsEmpty (k : ℕ) : k ≥ 3 → IsEmpty (ℒₒᵣ.Func k)

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.ORing.instEncodableRelORing (k : ℕ) : Encodable (ℒₒᵣ.Rel k)

Equations

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

def PointwiseComposition.FFL.FirstOrder.Language.ORing.funcEquivFinFour : (k : ℕ) × ℒₒᵣ.Func k ≃ Fin 4

The func Equiv Fin Four construction in FFL.FirstOrder.Language.ORing.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Language.ORing.relEquivFinTwo : (k : ℕ) × ℒₒᵣ.Rel k ≃ Fin 2

The rel Equiv Fin Two construction in FFL.FirstOrder.Language.ORing.

Equations

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

inductive PointwiseComposition.FFL.FirstOrder.Language.Constant.Func (C : Type u_1) : ℕ → Type u_1

Data and laws for Func in FFL.FirstOrder.Language.Constant.

• const {C : Type u_1} (c : C) : Func C 0

def PointwiseComposition.FFL.FirstOrder.Language.ofConstants (C : Type u_1) : Language

The of Constants construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.ofConstants C = { Func := PointwiseComposition.FFL.FirstOrder.Language.Constant.Func C, Rel := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instCoeFuncOfConstantsOfNatNat (C : Type u_1) : Coe C ((ofConstants C).Func 0)

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instCoeFuncOfConstantsOfNatNat C = { coe := PointwiseComposition.FFL.FirstOrder.Language.Constant.Func.const }

instance PointwiseComposition.FFL.FirstOrder.Language.instIsConstantOfConstants (C : Type u_1) : (ofConstants C).IsConstant

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Language.unit : Language

The unit construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.unit = PointwiseComposition.FFL.FirstOrder.Language.ofConstants PUnit.{?u.1 + 1}

def PointwiseComposition.FFL.FirstOrder.Language.ofFunc (F : ℕ → Type v) : Language

The of Func construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.ofFunc F = { Func := F, Rel := fun (x : ℕ) => PEmpty.{?u.1 + 1} }

def PointwiseComposition.FFL.FirstOrder.Language.add (L₁ : Language) (L₂ : Language) : Language

The add construction in FFL.FirstOrder.Language.

Equations

• L₁.add L₂ = { Func := fun (k : ℕ) => L₁.Func k ⊕ L₂.Func k, Rel := fun (k : ℕ) => L₁.Rel k ⊕ L₂.Rel k }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instAdd : Add Language

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instAdd = { add := PointwiseComposition.FFL.FirstOrder.Language.add }

def PointwiseComposition.FFL.FirstOrder.Language.sigma {ι : Type u_1} (L : ι → Language) : Language

The sigma construction in FFL.FirstOrder.Language.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.sigma L = { Func := fun (k : ℕ) => (i : ι) × (L i).Func k, Rel := fun (k : ℕ) => (i : ι) × (L i).Rel k }

class PointwiseComposition.FFL.FirstOrder.Language.Eq (L : Language) : Type u_1

Data and laws for Eq in FFL.FirstOrder.Language.

• eq : L.Rel 2

  The eq construction in FFL.FirstOrder.Language.Eq.

class PointwiseComposition.FFL.FirstOrder.Language.LT (L : Language) : Type u_1

Data and laws for LT in FFL.FirstOrder.Language.

• lt : L.Rel 2

  The lt construction in FFL.FirstOrder.Language.LT.

class PointwiseComposition.FFL.FirstOrder.Language.Mem (L : Language) : Type u_1

Data and laws for Mem in FFL.FirstOrder.Language.

• mem : L.Rel 2

  The mem construction in FFL.FirstOrder.Language.Mem.

class PointwiseComposition.FFL.FirstOrder.Language.Zero (L : Language) : Type u_1

Data and laws for Zero in FFL.FirstOrder.Language.

• zero : L.Func 0

  The zero construction in FFL.FirstOrder.Language.Zero.

class PointwiseComposition.FFL.FirstOrder.Language.One (L : Language) : Type u_1

Data and laws for One in FFL.FirstOrder.Language.

• one : L.Func 0

  The one construction in FFL.FirstOrder.Language.One.

class PointwiseComposition.FFL.FirstOrder.Language.Add (L : Language) : Type u_1

Data and laws for Add in FFL.FirstOrder.Language.

• add : L.Func 2

  The add construction in FFL.FirstOrder.Language.Add.

class PointwiseComposition.FFL.FirstOrder.Language.Mul (L : Language) : Type u_1

Data and laws for Mul in FFL.FirstOrder.Language.

• mul : L.Func 2

  The mul construction in FFL.FirstOrder.Language.Mul.

class PointwiseComposition.FFL.FirstOrder.Language.Pow (L : Language) : Type u_1

Data and laws for Pow in FFL.FirstOrder.Language.

• pow : L.Func 2

  The pow construction in FFL.FirstOrder.Language.Pow.

class PointwiseComposition.FFL.FirstOrder.Language.Exp (L : Language) : Type u_1

Data and laws for Exp in FFL.FirstOrder.Language.

• exp : L.Func 1

  The exp construction in FFL.FirstOrder.Language.Exp.

class PointwiseComposition.FFL.FirstOrder.Language.Pairing (L : Language) : Type u_1

Data and laws for Pairing in FFL.FirstOrder.Language.

• pair : L.Func 2

  The pair construction in FFL.FirstOrder.Language.Pairing.

class PointwiseComposition.FFL.FirstOrder.Language.Star (L : Language) : Type u_1

Data and laws for Star in FFL.FirstOrder.Language.

• star : L.Func 0

  The star construction in FFL.FirstOrder.Language.Star.

class PointwiseComposition.FFL.FirstOrder.Language.ORing (L : Language) extends L.Eq, L.LT, L.Zero, L.One, L.Add, L.Mul : Type u_1

Data and laws for ORing in FFL.FirstOrder.Language.

• eq : L.Rel 2
• lt : L.Rel 2
• zero : L.Func 0
• one : L.Func 0
• add : L.Func 2
• mul : L.Func 2

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instORingORing : ℒₒᵣ.ORing

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instConstantInhabitedORing : ℒₒᵣ.ConstantInhabited

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instConstantInhabitedORing = { default := PointwiseComposition.FFL.FirstOrder.Language.Zero.zero }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instStarUnit : unit.Star

Equations

• PointwiseComposition.FFL.FirstOrder.Language.instStarUnit = { star := PointwiseComposition.FFL.FirstOrder.Language.Constant.Func.const () }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instStarAdd (L : Language) (S : Language) [S.Star] : (L.add S).Star

Equations

• L.instStarAdd S = { star := Sum.inr PointwiseComposition.FFL.FirstOrder.Language.Star.star }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instZeroAdd (L : Language) (S : Language) [L.Zero] : (L.add S).Zero

Equations

• L.instZeroAdd S = { zero := Sum.inl PointwiseComposition.FFL.FirstOrder.Language.Zero.zero }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instOneAdd (L : Language) (S : Language) [L.One] : (L.add S).One

Equations

• L.instOneAdd S = { one := Sum.inl PointwiseComposition.FFL.FirstOrder.Language.One.one }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instAddAdd (L : Language) (S : Language) [L.Add] : (L.add S).Add

Equations

• L.instAddAdd S = { add := Sum.inl PointwiseComposition.FFL.FirstOrder.Language.Add.add }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instMulAdd (L : Language) (S : Language) [L.Mul] : (L.add S).Mul

Equations

• L.instMulAdd S = { mul := Sum.inl PointwiseComposition.FFL.FirstOrder.Language.Mul.mul }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instEqAdd (L : Language) (S : Language) [L.Eq] : (L.add S).Eq

Equations

• L.instEqAdd S = { eq := Sum.inl PointwiseComposition.FFL.FirstOrder.Language.Eq.eq }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Language.instLTAdd (L : Language) (S : Language) [L.LT] : (L.add S).LT

Equations

• L.instLTAdd S = { lt := Sum.inl PointwiseComposition.FFL.FirstOrder.Language.LT.lt }

structure PointwiseComposition.FFL.FirstOrder.Language.Hom (L₁ : Language) (L₂ : Language) : Type (max u_1 u_2)

Data and laws for Hom in FFL.FirstOrder.Language.

• func {k : ℕ} : L₁.Func k → L₂.Func k

  The func construction in FFL.FirstOrder.Language.Hom.

• rel {k : ℕ} : L₁.Rel k → L₂.Rel k

  The rel construction in FFL.FirstOrder.Language.Hom.

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.ext {L₁ : Language} {L₂ : Language} {x y : L₁.Hom L₂} (func : @func L₁ L₂ x = @func L₁ L₂ y) (rel : @rel L₁ L₂ x = @rel L₁ L₂ y) : x = y

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.ext_iff {L₁ : Language} {L₂ : Language} {x y : L₁.Hom L₂} : x = y ↔ @func L₁ L₂ x = @func L₁ L₂ y ∧ @rel L₁ L₂ x = @rel L₁ L₂ y

def PointwiseComposition.FFL.FirstOrder.«term_→ᵥ_» : Lean.TrailingParserDescr

A structure for the homomorphisms (respecting function and relation symbols) between first-order languages.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Language.Hom.id (L : Language) : L.Hom L

The id construction in FFL.FirstOrder.Language.Hom.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.Hom.id L = { func := fun {k : ℕ} => id, rel := fun {k : ℕ} => id }

def PointwiseComposition.FFL.FirstOrder.Language.Hom.comp {L₁ : Language} {L₂ : Language} {L₃ : Language} (Ψ : L₂.Hom L₃) (Φ : L₁.Hom L₂) : L₁.Hom L₃

The comp construction in FFL.FirstOrder.Language.Hom.

Equations

• Ψ.comp Φ = { func := fun {k : ℕ} => Ψ.func ∘ Φ.func, rel := fun {k : ℕ} => Ψ.rel ∘ Φ.rel }

def PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁ (L₁ : Language) (L₂ : Language) : L₁.Hom (L₁.add L₂)

The add₁ construction in FFL.FirstOrder.Language.Hom.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁ L₁ L₂ = { func := fun {k : ℕ} => Sum.inl, rel := fun {k : ℕ} => Sum.inl }

def PointwiseComposition.FFL.FirstOrder.Language.Hom.add₂ (L₁ : Language) (L₂ : Language) : L₂.Hom (L₁.add L₂)

The add₂ construction in FFL.FirstOrder.Language.Hom.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.Hom.add₂ L₁ L₂ = { func := fun {k : ℕ} => Sum.inr, rel := fun {k : ℕ} => Sum.inr }

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.func_add₁ {k : ℕ} (L₁ : Language) (L₂ : Language) (f : L₁.Func k) : (add₁ L₁ L₂).func f = Sum.inl f

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.rel_add₁ {k : ℕ} (L₁ : Language) (L₂ : Language) (r : L₁.Rel k) : (add₁ L₁ L₂).rel r = Sum.inl r

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.func_add₂ {k : ℕ} (L₁ : Language) (L₂ : Language) (f : L₂.Func k) : (add₂ L₁ L₂).func f = Sum.inr f

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.rel_add₂ {k : ℕ} (L₁ : Language) (L₂ : Language) (r : L₂.Rel k) : (add₂ L₁ L₂).rel r = Sum.inr r

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.add₂_star (L₁ : Language) (L₂ : Language) [L₂.Star] : (add₂ L₁ L₂).func Star.star = Star.star

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁_zero (L₁ : Language) (L₂ : Language) [L₁.Zero] : (add₁ L₁ L₂).func Zero.zero = Zero.zero

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁_one (L₁ : Language) (L₂ : Language) [L₁.One] : (add₁ L₁ L₂).func One.one = One.one

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁_add (L₁ : Language) (L₂ : Language) [L₁.Add] : (add₁ L₁ L₂).func Add.add = Add.add

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁_mul (L₁ : Language) (L₂ : Language) [L₁.Mul] : (add₁ L₁ L₂).func Mul.mul = Mul.mul

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁_eq (L₁ : Language) (L₂ : Language) [L₁.Eq] : (add₁ L₁ L₂).rel Eq.eq = Eq.eq

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.add₁_lt (L₁ : Language) (L₂ : Language) [L₁.LT] : (add₁ L₁ L₂).rel LT.lt = LT.lt

def PointwiseComposition.FFL.FirstOrder.Language.Hom.sigma {ι : Type u_1} (L : ι → Language) (i : ι) : (L i).Hom (Language.sigma L)

The sigma construction in FFL.FirstOrder.Language.Hom.

Equations

• PointwiseComposition.FFL.FirstOrder.Language.Hom.sigma L i = { func := fun {k : ℕ} (f : (L i).Func k) => ⟨i, f⟩, rel := fun {k : ℕ} (r : (L i).Rel k) => ⟨i, r⟩ }

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.func_sigma {ι : Type u_1} {k : ℕ} (L : ι → Language) (i : ι) (f : (L i).Func k) : (sigma L i).func f = ⟨i, f⟩

theorem PointwiseComposition.FFL.FirstOrder.Language.Hom.rel_sigma {ι : Type u_1} {k : ℕ} (L : ι → Language) (i : ι) (r : (L i).Rel k) : (sigma L i).rel r = ⟨i, r⟩

def PointwiseComposition.FFL.FirstOrder.Language.ORing.embedding (L : Language) [L.ORing] : ℒₒᵣ.Hom L

The embedding construction in FFL.FirstOrder.Language.ORing.

Equations

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

class PointwiseComposition.FFL.FirstOrder.Language.DecidableEq (L : Language) : Type u_1

Data and laws for Decidable Eq in FFL.FirstOrder.Language.

• func (k : ℕ) : DecidableEq (L.Func k)

  The func construction in FFL.FirstOrder.Language.DecidableEq.

• rel (k : ℕ) : DecidableEq (L.Rel k)

  The rel construction in FFL.FirstOrder.Language.DecidableEq.

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instDecidableEqOfFuncOfDecidableEqRel (L : Language) [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] : L.DecidableEq

Equations

• PointwiseComposition.FFL.FirstOrder.instDecidableEqOfFuncOfDecidableEqRel L = { func := fun (x : ℕ) => inferInstance, rel := fun (x : ℕ) => inferInstance }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instDecidableEqFuncOfDecidableEq (L : Language) [L.DecidableEq] (k : ℕ) : DecidableEq (L.Func k)

Equations

• PointwiseComposition.FFL.FirstOrder.instDecidableEqFuncOfDecidableEq L k = PointwiseComposition.FFL.FirstOrder.Language.DecidableEq.func k

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instDecidableEqRelOfDecidableEq (L : Language) [L.DecidableEq] (k : ℕ) : DecidableEq (L.Rel k)

Equations

• PointwiseComposition.FFL.FirstOrder.instDecidableEqRelOfDecidableEq L k = PointwiseComposition.FFL.FirstOrder.Language.DecidableEq.rel k

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instDecidableEqRelOfDecidableEq_1 (L : Language) [L.DecidableEq] (k : ℕ) : DecidableEq (L.Rel k)

Equations

• PointwiseComposition.FFL.FirstOrder.instDecidableEqRelOfDecidableEq_1 L k = PointwiseComposition.FFL.FirstOrder.Language.DecidableEq.rel k

class PointwiseComposition.FFL.FirstOrder.Language.Encodable (L : Language) : Type u_1

Data and laws for Encodable in FFL.FirstOrder.Language.

• func (k : ℕ) : Encodable (L.Func k)

  The func construction in FFL.FirstOrder.Language.Encodable.

• rel (k : ℕ) : Encodable (L.Rel k)

  The rel construction in FFL.FirstOrder.Language.Encodable.

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instEncodableOfFuncOfEncodableRel (L : Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] : L.Encodable

Equations

• PointwiseComposition.FFL.FirstOrder.instEncodableOfFuncOfEncodableRel L = { func := fun (x : ℕ) => inferInstance, rel := fun (x : ℕ) => inferInstance }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instEncodableFuncOfEncodable (L : Language) [L.Encodable] (k : ℕ) : Encodable (L.Func k)

Equations

• PointwiseComposition.FFL.FirstOrder.instEncodableFuncOfEncodable L k = PointwiseComposition.FFL.FirstOrder.Language.Encodable.func k

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instEncodableRelOfEncodable (L : Language) [L.Encodable] (k : ℕ) : Encodable (L.Rel k)

Equations

• PointwiseComposition.FFL.FirstOrder.instEncodableRelOfEncodable L k = PointwiseComposition.FFL.FirstOrder.Language.Encodable.rel k

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instEncodableRelOfEncodable_1 (L : Language) [L.Encodable] (k : ℕ) : Encodable (L.Rel k)

Equations

• PointwiseComposition.FFL.FirstOrder.instEncodableRelOfEncodable_1 L k = PointwiseComposition.FFL.FirstOrder.Language.Encodable.rel k

class PointwiseComposition.FFL.FirstOrder.Language.Finite (L : Language) : Type u_1

Data and laws for Finite in FFL.FirstOrder.Language.

• func : Fintype ((k : ℕ) × L.Func k)

  The func construction in FFL.FirstOrder.Language.Finite.

• rel : Fintype ((k : ℕ) × L.Rel k)

  The rel construction in FFL.FirstOrder.Language.Finite.

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.instFiniteORing : ℒₒᵣ.Finite

Equations

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