Documentation

Lean 4 Proof

theorem hysteresisWidth_increasing_in_complementarity
    {ρ₁ ρ₂ : ℝ} (hρ : ρ₁ < ρ₂) {bf : ℝ} (hbf : 0 < bf) :
    hysteresisWidth ρ₂ bf < hysteresisWidth ρ₁ bf := by
  simp only [hysteresisWidth]
  nlinarith

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:77

Module Section

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

In the same file