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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

• 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 FFL.FirstOrder.Theory.«term𝗘𝗤» : Lean.ParserDescr

Equations

• FFL.FirstOrder.Theory.«term𝗘𝗤» = Lean.ParserDescr.node `FFL.FirstOrder.Theory.«term𝗘𝗤» 1024 (Lean.ParserDescr.symbol "𝗘𝗤")

theorem 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 FFL.FirstOrder.Theory.EqAxiom.finite {L : Language} [Semiformula.Operator.Eq L] [L.Finite] : Set.Finite (𝗘𝗤 L)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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