IndisputableMonolith.Causality.BoundedStep

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4
   5/-- Locally-finite step relation with bounded out-degree. -/
   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
  13