noncomputable def LO.FirstOrder.Arithmetic.finsetArithmetizeAux {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : List V → V

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.finsetArithmetizeAux_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : finsetArithmetizeAux [] = ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.finsetArithmetizeAux_cons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x : V) (xs : List V) : finsetArithmetizeAux (x :: xs) = insert x (finsetArithmetizeAux xs)

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_finsetArithmetizeAux_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x : V} {s : List V} : x ∈ finsetArithmetizeAux s ↔ x ∈ s

noncomputable def Finset.arithmetize {V : Type u_1} [LO.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : Finset V) : V

Equations

• s.arithmetize = LO.FirstOrder.Arithmetic.finsetArithmetizeAux s.toList

@[simp]

theorem LO.FirstOrder.Arithmetic.mem_finsetArithmetize_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {x : V} {s : Finset V} : x ∈ s.arithmetize ↔ x ∈ s

@[simp]

theorem LO.FirstOrder.Arithmetic.finset_empty_arithmetize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : ∅.arithmetize = ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.finset_insert_arithmetize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) (s : Finset V) : (insert a s).arithmetize = insert a s.arithmetize