Documentation

Lean 4 Proof

theorem fragility_total {ρ : ℝ} (hρ : ρ ≤ 0) :
    fragilityIndex J ρ = 1 := by
  simp only [fragilityIndex]
  rw [knockout_total_failure hρ (by omega : 0 < 1)]
  ring

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:173

Module Section

Propositions 12-17 and Corollary 5:

In the same file