Documentation

Lean 4 Proof

theorem sigma_substitutes {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) :
    1 < elasticityOfSubstitution ρ :=
  sigma_gt_one hρ hρ1

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:98

Module Section

Economics extensions for CES formalization:

In the same file