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)
8structure Kinematics (α : Type) where
9 step : α → α → Prop
10
used by (37)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ballP
in IndisputableMonolith.Causality.BallP
decl_use
-
ballP_mono
in IndisputableMonolith.Causality.BallP
decl_use
-
ballP_subset_inBall
in IndisputableMonolith.Causality.BallP
decl_use
-
inBall_subset_ballP
in IndisputableMonolith.Causality.BallP
decl_use
-
reach_mem_ballP
in IndisputableMonolith.Causality.BallP
decl_use
-
inBall
in IndisputableMonolith.Causality.Basic
decl_use
-
inBall_mono
in IndisputableMonolith.Causality.Basic
decl_use
-
Reaches
in IndisputableMonolith.Causality.Basic
decl_use
-
reaches_of_reachN
in IndisputableMonolith.Causality.Basic
decl_use
-
reach_in_ball
in IndisputableMonolith.Causality.Basic
decl_use
-
reach_le_in_ball
in IndisputableMonolith.Causality.Basic
decl_use
-
ReachN
in IndisputableMonolith.Causality.Basic
decl_use
-
ballP
in IndisputableMonolith.Causality.ConeBound
decl_use
-
KB
in IndisputableMonolith.Causality.ConeBound
decl_use
-
Kinematics
in IndisputableMonolith.Causality.ConeBound
decl_use
-
ballP
in IndisputableMonolith.Causality.Reach
decl_use
-
ballP_mono
in IndisputableMonolith.Causality.Reach
decl_use
-
ballP_subset_inBall
in IndisputableMonolith.Causality.Reach
decl_use
-
inBall
in IndisputableMonolith.Causality.Reach
decl_use
-
inBall_mono
in IndisputableMonolith.Causality.Reach
decl_use
-
inBall_subset_ballP
in IndisputableMonolith.Causality.Reach
decl_use
-
Kinematics
in IndisputableMonolith.Causality.Reach
decl_use
-
Reaches
in IndisputableMonolith.Causality.Reach
decl_use
-
reaches_of_reachN
in IndisputableMonolith.Causality.Reach
decl_use
-
reach_in_ball
in IndisputableMonolith.Causality.Reach
decl_use
-
reach_le_in_ball
in IndisputableMonolith.Causality.Reach
decl_use
-
reach_mem_ballP
in IndisputableMonolith.Causality.Reach
decl_use
-
ReachN
in IndisputableMonolith.Causality.Reach
decl_use
-
ConeEntropyFacts
in IndisputableMonolith.ConeExport.Theorem
decl_use
-
inBall
in IndisputableMonolith.LedgerUniqueness
decl_use
… and 7 more
depends on (5)
Lean names referenced from this declaration's body.
-
Kinematics
in IndisputableMonolith.Causality.ConeBound
decl_use
-
Kinematics
in IndisputableMonolith.Causality.Reach
decl_use
-
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
Kinematics
in IndisputableMonolith.LedgerUniqueness
decl_use
-
Kinematics
in IndisputableMonolith.LightCone.StepBounds
decl_use