Documentation

Lean 4 Proof

theorem cesSlutky_symmetric (σ : ℝ) (s : Fin J → ℝ) (j k : Fin J) :
    cesSlutkyTerm σ s j k = cesSlutkyTerm σ s k j := by
  simp only [cesSlutkyTerm]
  by_cases hjk : j = k
  · subst hjk; ring
  · simp only [hjk, Ne.symm hjk, ite_false]; ring

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:891

Module Section

Economics extensions for CES formalization:

In the same file