Documentation

Lean 4 Proof

theorem hysteresisWidth_pos {ρ : ℝ} (hρ : ρ < 1) {bf : ℝ} (hbf : 0 < bf) :
    0 < hysteresisWidth ρ bf := by
  simp only [hysteresisWidth]
  exact mul_pos (by linarith) hbf

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:70

Module Section

## Entry-Exit Core Definitions (merged from EntryExitDefs.lean)

In the same file