Documentation

Lean 4 Proof

def AxiomA3_Symmetry (Φ : (Fin J → ℝ) → (Fin J → ℝ) → ℝ) : Prop :=
  ∀ (ε : Fin J → ℝ) (σ : Equiv.Perm (Fin J)),
    (∀ j, ε (σ j) = ε j) →
    ∀ p : Fin J → ℝ, Φ (p ∘ σ) ε = Φ p ε

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:49

Module Section

Theorem 3: CES Potential Uniqueness (Paper 2, Section 3.2)

In the same file