Coding

def LO.Arith.finsetArithmetizeAux {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : List V → V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.finsetArithmetizeAux [] = ∅
• LO.Arith.finsetArithmetizeAux (x_1 :: xs) = insert x_1 (LO.Arith.finsetArithmetizeAux xs)

@[simp]

theorem LO.Arith.finsetArithmetizeAux_nil {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : finsetArithmetizeAux [] = ∅

@[simp]

theorem LO.Arith.finsetArithmetizeAux_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (x : V) (xs : List V) : finsetArithmetizeAux (x :: xs) = insert x (finsetArithmetizeAux xs)

@[simp]

theorem LO.Arith.mem_finsetArithmetizeAux_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {x : V} {s : List V} : x ∈ finsetArithmetizeAux s ↔ x ∈ s

noncomputable def Finset.arithmetize {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s : Finset V) : V

Imported declaration from the Incompleteness formalization.

Equations

• s.arithmetize = LO.Arith.finsetArithmetizeAux s.toList

@[simp]

theorem LO.Arith.mem_finsetArithmetize_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {x : V} {s : Finset V} : x ∈ s.arithmetize ↔ x ∈ s

@[simp]

theorem LO.Arith.finset_empty_arithmetize {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : ∅.arithmetize = ∅

@[simp]

theorem LO.Arith.finset_insert_arithmetize {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (a : V) (s : Finset V) : (insert a s).arithmetize = insert a s.arithmetize