def definition def or abbrev

`neighbors`

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

formal statement (Lean)

  18def neighbors (G : StakeGraph) (nodes : List Stakeholder) (s : Stakeholder) : List Stakeholder :=

Definition body.

  19  nodes.filter (fun t => G.edge s t)
  20

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

BoundedStep in IndisputableMonolith.Causality.BoundedStep decl_use
ballFS in IndisputableMonolith.Causality.ConeBound decl_use
BoundedStep in IndisputableMonolith.Causality.ConeBound decl_use
card_ballFS_succ_le in IndisputableMonolith.Causality.ConeBound decl_use
card_bind_neighbors_le in IndisputableMonolith.Causality.ConeBound decl_use
mem_ballFS_iff_ballP in IndisputableMonolith.Causality.ConeBound decl_use
sum_card_neighbors_le in IndisputableMonolith.Causality.ConeBound decl_use
reachable in IndisputableMonolith.Ethics.StakeGraph decl_use
MediumState in IndisputableMonolith.Flight.Medium decl_use
geometricMean_pos in IndisputableMonolith.Foundation.JCostGeometry decl_use
geometric_ne_arithmetic in IndisputableMonolith.Foundation.JCostGeometry decl_use
totalJcost in IndisputableMonolith.Foundation.JCostGeometry decl_use
V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
finite_resolution_mono in IndisputableMonolith.RecogGeom.FiniteResolution decl_use
SimpleTicks in IndisputableMonolith.Recognition.ModelingExamples decl_use

Lean names referenced from this declaration's body.