Documentation

Arithmetization.Vorspiel.Vorspiel

Equations
  • =
theorem Matrix.forall_iff {α : Type u_1} {n : } (p : (Fin (n + 1)α)Prop) :
(∀ (v : Fin (n + 1)α), p v) ∀ (a : α) (v : Fin nα), p (a :> v)
theorem Matrix.comp_vecCons₂' {β : Sort u_1} {γ : Type u_2} {α : Type u_3} {n : } (g : βγ) (f : αβ) (a : α) (s : Fin nα) :
(fun (x : Fin n.succ) => g (f ((a :> s) x))) = g (f a) :> fun (i : Fin n) => g (f (s i))
@[simp]
theorem Set.subset_union_three₁ {α : Type u_1} (s : Set α) (t : Set α) (u : Set α) :
s s t u
@[simp]
theorem Set.subset_union_three₂ {α : Type u_1} (s : Set α) (t : Set α) (u : Set α) :
t s t u
@[simp]
theorem Set.subset_union_three₃ {α : Type u_1} (s : Set α) (t : Set α) (u : Set α) :
u s t u
theorem Matrix.fun_eq_vec₃ {α : Type u_1} {v : Fin 3α} :
v = ![v 0, v 1, v 2]
theorem Matrix.fun_eq_vec₄ {α : Type u_1} {v : Fin 4α} :
v = ![v 0, v 1, v 2, v 3]
@[simp]
theorem Matrix.cons_app_four {α : Type u_1} {n : } (a : α) (s : Fin n.succ.succ.succ.succα) :
(a :> s) 4 = s 3
@[simp]
theorem Matrix.cons_app_five {α : Type u_1} {n : } (a : α) (s : Fin n.succ.succ.succ.succ.succα) :
(a :> s) 5 = s 4
@[simp]
theorem Matrix.cons_app_six {α : Type u_1} {n : } (a : α) (s : Fin n.succ.succ.succ.succ.succ.succα) :
(a :> s) 6 = s 5
@[simp]
theorem Matrix.cons_app_seven {α : Type u_1} {n : } (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succα) :
(a :> s) 7 = s 6
@[simp]
theorem Matrix.cons_app_eight {α : Type u_1} {n : } (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succα) :
(a :> s) 8 = s 7
theorem Matrix.eq_vecCons' {n : } {C : Type u_1} (s : Fin (n + 1)C) :
(s 0 :> fun (x : Fin n) => s x.succ) = s
theorem forall_fin_iff_zero_and_forall_succ {k : } {P : Fin (k + 1)Prop} :
(∀ (i : Fin (k + 1)), P i) P 0 ∀ (i : Fin k), P i.succ
theorem exists_fin_iff_zero_or_exists_succ {k : } {P : Fin (k + 1)Prop} :
(∃ (i : Fin (k + 1)), P i) P 0 ∃ (i : Fin k), P i.succ
theorem forall_vec_iff_forall_forall_vec {k : } {α : Type u_1} {P : (Fin (k + 1)α)Prop} :
(∀ (v : Fin (k + 1)α), P v) ∀ (x : α) (v : Fin kα), P (x :> v)
theorem exists_vec_iff_exists_exists_vec {k : } {α : Type u_1} {P : (Fin (k + 1)α)Prop} :
(∃ (v : Fin (k + 1)α), P v) ∃ (x : α) (v : Fin kα), P (x :> v)
theorem exists_le_vec_iff_exists_le_exists_vec {α : Type u_1} {k : } [LE α] {P : (Fin (k + 1)α)Prop} {f : Fin (k + 1)α} :
(vf, P v) xf 0, vfun (x : Fin k) => f x.succ, P (x :> v)
theorem forall_le_vec_iff_forall_le_forall_vec {α : Type u_1} {k : } [LE α] {P : (Fin (k + 1)α)Prop} {f : Fin (k + 1)α} :
(vf, P v) xf 0, vfun (x : Fin k) => f x.succ, P (x :> v)
class Hash (α : Type u_1) :
Type u_1
  • hash : ααα
Instances
    class Length (α : Type u_1) :
    Type u_1
    • length : αα
    Instances
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def LO.Polarity.coe {α : Type u_1} [LO.SigmaSymbol α] [LO.PiSymbol α] :
        Equations
        Instances For
          Equations
          • LO.Polarity.instCoe_arithmetization = { coe := LO.Polarity.coe }
          @[simp]
          theorem LO.Polarity.coe_sigma {α : Type u_1} [LO.SigmaSymbol α] [LO.PiSymbol α] :
          𝚺.coe = 𝚺
          @[simp]
          theorem LO.Polarity.coe_pi {α : Type u_1} [LO.SigmaSymbol α] [LO.PiSymbol α] :
          𝚷.coe = 𝚷
          @[simp]
          theorem LO.SigmaPiDelta.alt_coe (Γ : LO.Polarity) :
          Γ.coe.alt = Γ.alt.coe
          Equations
          Equations
          • LO.FirstOrder.Arith.instToStringSemitermORing_arithmetization = { toString := LO.FirstOrder.Arith.termToStr }
          Equations
          Equations
          • LO.FirstOrder.Arith.instToStringSemiformulaORing_arithmetization = { toString := LO.FirstOrder.Arith.formulaToStr }
          @[simp]
          theorem LO.FirstOrder.Semiformula.eval_operator₃ {ξ : Type u_3} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {n : } {ε : ξM} {e : Fin nM} {o : LO.FirstOrder.Semiformula.Operator L 3} {t₁ : LO.FirstOrder.Semiterm L ξ n} {t₂ : LO.FirstOrder.Semiterm L ξ n} {t₃ : LO.FirstOrder.Semiterm L ξ n} :
          (LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t₁, t₂, t₃]) o.val ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂, LO.FirstOrder.Semiterm.val s e ε t₃]
          @[simp]
          theorem LO.FirstOrder.Semiformula.eval_operator₄ {ξ : Type u_3} {L : LO.FirstOrder.Language} {M : Type u_1} {s : LO.FirstOrder.Structure L M} {n : } {ε : ξM} {e : Fin nM} {o : LO.FirstOrder.Semiformula.Operator L 4} {t₁ : LO.FirstOrder.Semiterm L ξ n} {t₂ : LO.FirstOrder.Semiterm L ξ n} {t₃ : LO.FirstOrder.Semiterm L ξ n} {t₄ : LO.FirstOrder.Semiterm L ξ n} :
          (LO.FirstOrder.Semiformula.Eval s e ε) (o.operator ![t₁, t₂, t₃, t₄]) o.val ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂, LO.FirstOrder.Semiterm.val s e ε t₃, LO.FirstOrder.Semiterm.val s e ε t₄]
          @[reducible, inline]
          abbrev LO.FirstOrder.Semiterm.Rlz {L : LO.FirstOrder.Language} {M : Type u_1} [LO.FirstOrder.Structure L M] {n : } (t : LO.FirstOrder.Semiterm L M n) (e : Fin nM) :
          M
          Equations
          Instances For
            @[reducible, inline]
            Equations
            Instances For
              @[simp]
              theorem Mathlib.Vector.nil_get {α : Type u_1} (v : Mathlib.Vector α 0) :
              v.get = ![]