Documentation

Lean 4 Proof

theorem ceiling_nonneg {phi_prev sigma_n : ℝ}
    (hphi : 0 ≤ phi_prev) (hs : 0 < sigma_n) :
    0 ≤ phi_prev / sigma_n :=
  div_nonneg hphi (le_of_lt hs)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/TransitionDynamics.lean:38

Module Section

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

In the same file