Documentation

Lean 4 Proof

theorem perCapitaSurplus_pos {J ρ : ℝ} (hJ : 1 < J) (hρ : ρ < 1) :
    0 < perCapitaSurplus J ρ := by
  simp only [perCapitaSurplus]
  apply div_pos
  · exact mul_pos (by linarith) (by linarith)
  · exact sq_pos_of_pos (by linarith)

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:184

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)

In the same file