121theorem isBankrupt_antimono {n : ℕ} (E : Ecosystem n) 122 (L₁ L₂ : Finset (Fin n)) (h : L₁ ⊆ L₂) (j : Fin n) : 123 IsBankrupt E L₂ j → IsBankrupt E L₁ j := by
proof body
Tactic-mode proof.
124 unfold IsBankrupt totalRung 125 intro hbk 126 have hsum : L₁.sum (fun i => E.support i j) ≤ 127 L₂.sum (fun i => E.support i j) := by 128 apply Finset.sum_le_sum_of_subset_of_nonneg h 129 intro i _ _ 130 exact E.support_nonneg i j 131 linarith 132 133/-! ## §4. Cascade-closure step -/ 134 135/-- One step of the cascade: removes from the live set every species 136that is bankrupt under the current live set. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.