Documentation

Lean 4 Proof

theorem hysteresis_width_positive {ρ : ℝ} (hρ : ρ < 1)
    {bf : ℝ} (hbf : 0 < bf) :
    0 < hysteresisWidth ρ bf :=
  hysteresisWidth_pos hρ hbf

Dependency Graph

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:78

Module Section

Paper 3c, Section 3: First-Order Regime Shift

In the same file