Documentation

Lean 4 Proof

theorem perCapitaBenefit_pos {J ρ c : ℝ} (hJ : 0 < J) (hc : 0 < c) :
    0 < perCapitaBenefit J ρ c := by
  simp only [perCapitaBenefit]
  exact mul_pos (rpow_pos_of_pos hJ _) hc

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:60

Module Section

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

In the same file