theorem
other
other
cascadeIterate_zero
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)
159theorem cascadeIterate_zero {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
160 cascadeIterate E L 0 = L := rfl
depends on (5)
Lean names referenced from this declaration's body.
-
cascadeIterate
in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy
decl_use
-
Ecosystem
in IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy
decl_use
-
E
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use