pith. machine review for the scientific record. sign in
theorem proved term proof

cascadeIterate_subset_initial

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 170theorem cascadeIterate_subset_initial {n : ℕ} (E : Ecosystem n)
 171    (L : Finset (Fin n)) (k : ℕ) :
 172    cascadeIterate E L k ⊆ L := by

proof body

Term-mode proof.

 173  induction k with
 174  | zero => simp [cascadeIterate]
 175  | succ k ih =>
 176      apply Finset.Subset.trans (cascadeIterate_subset E L k) ih
 177

depends on (8)

Lean names referenced from this declaration's body.