Documentation

Lean 4 Proof

theorem curvature_correction {phi_prev K : ℝ} (hphi : 0 < phi_prev) (hK : 0 < K) :
    0 < K * phi_prev :=
  mul_pos hK hphi

Dependency Graph

Location

thesis/CESProofs/Hierarchy/TransitionDynamics.lean:101

Module Section

Propositions 8-11, Theorems 10-12: Transition Dynamics

In the same file