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

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} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.finsetArithmetizeAux [] = ∅

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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