class definition def or abbrev

`BoundedStep`

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

formal statement (Lean)

   6class BoundedStep (α : Type) (degree_bound : outParam Nat) where
   7  step : α → α → Prop
   8  neighbors : α → Finset α
   9  step_iff_mem : ∀ x y, step x y ↔ y ∈ neighbors x
  10  degree_bound_holds : ∀ x, (neighbors x).card ≤ degree_bound
  11
  12end IndisputableMonolith

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

ballP in IndisputableMonolith.Causality.ConeBound decl_use
BoundedStep in IndisputableMonolith.Causality.ConeBound decl_use
SimpleTicks in IndisputableMonolith.Recognition.ModelingExamples decl_use

depends on (3)

Lean names referenced from this declaration's body.

BoundedStep in IndisputableMonolith.Causality.ConeBound decl_use
step in IndisputableMonolith.Complexity.CellularAutomata decl_use
neighbors in IndisputableMonolith.Ethics.StakeGraph decl_use