Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.HFS.Coding

Supporting results for pointwise provable equality.

source
noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.finsetArithmetizeAux {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] :
List V → V

The finset Arithmetize Aux construction in FFL.FirstOrder.Arithmetic.

Equations
Instances For
    source
    @[simp]
    theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.finsetArithmetizeAux_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] :
    finsetArithmetizeAux [] = ∅
    source
    @[simp]
    theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.finsetArithmetizeAux_cons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x : V) (xs : List V) :
    finsetArithmetizeAux (x :: xs) = insert x (finsetArithmetizeAux xs)
    source
    @[simp]
    theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mem_finsetArithmetizeAux_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x : V} {s : List V} :
    x ∈ finsetArithmetizeAux s ↔ x ∈ s
    source
    noncomputable def PointwiseComposition.Finset.arithmetize {V : Type u_1} [FFL.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (s : Finset V) :
    V

    The arithmetize construction in Finset.

    Equations
    Instances For
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mem_finsetArithmetize_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {x : V} {s : Finset V} :
      x ∈ Finset.arithmetize s ↔ x ∈ s
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.finset_empty_arithmetize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] :
      Finset.arithmetize ∅ = ∅
      source
      @[simp]
      theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.finset_insert_arithmetize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (a : V) (s : Finset V) :
      Finset.arithmetize (insert a s) = insert a (Finset.arithmetize s)