`cascadeStep_subset`

proved

show as: view math explainer →

module: IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy
domain: Ecology
line: 141 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy on GitHub at line 141.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 138    Finset (Fin n) :=
 139  L.filter (fun j => ¬ IsBankrupt E L j)
 140
 141theorem cascadeStep_subset {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
 142    cascadeStep E L ⊆ L := by
 143  unfold cascadeStep
 144  exact Finset.filter_subset _ _
 145
 146/-- Each cascade step weakly shrinks the live set. -/
 147theorem cascadeStep_card_le {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
 148    (cascadeStep E L).card ≤ L.card :=
 149  Finset.card_le_card (cascadeStep_subset E L)
 150
 151/-! ## §5. Iterated cascade closure -/
 152
 153/-- Iterate the cascade step `k` times. -/
 154def cascadeIterate {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
 155    ℕ → Finset (Fin n)
 156  | 0     => L
 157  | k + 1 => cascadeStep E (cascadeIterate E L k)
 158
 159theorem cascadeIterate_zero {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
 160    cascadeIterate E L 0 = L := rfl
 161
 162theorem cascadeIterate_succ {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ) :
 163    cascadeIterate E L (k + 1) = cascadeStep E (cascadeIterate E L k) := rfl
 164
 165theorem cascadeIterate_subset {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ) :
 166    cascadeIterate E L (k + 1) ⊆ cascadeIterate E L k := by
 167  rw [cascadeIterate_succ]
 168  exact cascadeStep_subset E (cascadeIterate E L k)
 169
 170theorem cascadeIterate_subset_initial {n : ℕ} (E : Ecosystem n)
 171    (L : Finset (Fin n)) (k : ℕ) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.