Documentation

Lean 4 Proof

theorem entryTimescale_pos {lambda lf : ℝ}
    (hlam : 0 < lambda) (hlf : 0 < lf) :
    0 < entryTimescale lambda lf := by
  simp only [entryTimescale]
  exact div_pos hlf hlam

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:237

Module Section

## Entry-Exit Dynamics

In the same file