Causality.Reach
IndisputableMonolith.Causality.Reach
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.ConeExport.Theorem
Kinematics
ReachN
inBall
reach_in_ball
reach_le_in_ball
Reaches
reaches_of_reachN
inBall_mono
ballP
ballP_mono
reach_mem_ballP
inBall_subset_ballP
ballP_subset_inBall