Causality.Basic
IndisputableMonolith.Causality.Basic
No prose has been written for this declaration yet. The Lean source and graph data below render without it.
generate prose now
From the project-wide theorem graph. These declarations reference this one in their body.
IndisputableMonolith.Causality.BallP
IndisputableMonolith.LedgerUniqueness
IndisputableMonolith.Potential
Kinematics
ReachN
inBall
reach_in_ball
reach_le_in_ball
Reaches
reaches_of_reachN
inBall_mono