Documentation

Lean 4 Proof

theorem weight_positive
    {N : ℕ} (e : WeightedHierarchicalCESEconomy N) (n : Fin N) (j : Fin (e.J n)) :
    0 < e.a n j := by
  exact e.ha_pos n j

Dependency Graph

Location

thesis/CESProofs/Hierarchy/KnockoutHierarchy.lean:50

Module Section

## Proposition 4b.4: Critical Supplier Identification

In the same file