Supporting results for pointwise provable equality.

def PointwiseComposition.Matrix.iget {α : Type u_1} {k : ℕ} [Inhabited α] (v : Fin k → α) (x : ℕ) : α

The iget construction in Matrix.

Equations

• PointwiseComposition.Matrix.iget v x = if h : x < k then v ⟨x, h⟩ else default

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Theory.Eq.refl (L : Language) [Semiformula.Operator.Eq L] : Sentence L

The refl construction in FFL.FirstOrder.Theory.Eq.

Equations

• PointwiseComposition.FFL.FirstOrder.Theory.Eq.refl L = (“∀¹ !!(PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0) = !!(PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0)”)

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Theory.Eq.symm (L : Language) [Semiformula.Operator.Eq L] : Sentence L

The symm construction in FFL.FirstOrder.Theory.Eq.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Theory.Eq.trans (L : Language) [Semiformula.Operator.Eq L] : Sentence L

The trans construction in FFL.FirstOrder.Theory.Eq.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Theory.Eq.funcExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k) : Sentence L

The func Ext construction in FFL.FirstOrder.Theory.Eq.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Theory.Eq.relExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k) : Sentence L

The rel Ext construction in FFL.FirstOrder.Theory.Eq.

Equations

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

inductive PointwiseComposition.FFL.FirstOrder.Theory.eqAxiom (L : Language) [Semiformula.Operator.Eq L] : Theory L

Data and laws for 𝐄𝐐 in 𝐄𝐐.

• refl {L : Language} [Semiformula.Operator.Eq L] : 𝐄𝐐 L (Eq.refl L)
• symm {L : Language} [Semiformula.Operator.Eq L] : 𝐄𝐐 L (Eq.symm L)
• trans {L : Language} [Semiformula.Operator.Eq L] : 𝐄𝐐 L (Eq.trans L)
• funcExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (f : L.Func k) : 𝐄𝐐 L (Eq.funcExt f)
• relExt {L : Language} [Semiformula.Operator.Eq L] {k : ℕ} (r : L.Rel k) : 𝐄𝐐 L (Eq.relExt r)

def PointwiseComposition.FFL.FirstOrder.Theory.«term𝐄𝐐» : Lean.ParserDescr

The «term𝐄𝐐» construction in FFL.FirstOrder.Theory.

Equations

• PointwiseComposition.FFL.FirstOrder.Theory.«term𝐄𝐐» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Theory.«term𝐄𝐐» 1024 (Lean.ParserDescr.symbol "𝐄𝐐")

theorem PointwiseComposition.FFL.FirstOrder.Theory.Eq.defeq {L : Language} [Semiformula.Operator.Eq L] : 𝐄𝐐 L = ({refl L, symm L, trans L} ∪ Set.range fun (f : (k : ℕ) × L.Func k) => funcExt f.snd) ∪ Set.range fun (f : (k : ℕ) × L.Rel k) => relExt f.snd

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Theory.EqAxiom.finite {L : Language} [Semiformula.Operator.Eq L] [L.Finite] : Set.Finite (𝐄𝐐 L)

def PointwiseComposition.FFL.FirstOrder.Semiformula.existsUnique {L : Language} [Operator.Eq L] {n : ℕ} {ξ : Type u_3} (φ : Semiformula L ξ (n + 1)) : Semiformula L ξ n

The exists Unique construction in FFL.FirstOrder.Semiformula.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Semiformula.«term∃¹!_» : Lean.ParserDescr

The «term∃¹! » construction in FFL.FirstOrder.Semiformula.

Equations

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

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃!_» : Lean.ParserDescr

The «first order formula∃! » construction in FFL.FirstOrder.BinderNotation.

Equations

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

def PointwiseComposition.FFL.FirstOrder.BinderNotation.«firstOrderFormula∃!_,_» : Lean.ParserDescr

The «first order formula∃! , » construction in FFL.FirstOrder.BinderNotation.

Equations

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