lemma
other
other
reach_in_ball
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)
18lemma reach_in_ball {K : Kinematics α} {x y : α} {n : Nat}
19 (h : ReachN K n x y) : inBall K x n y := ⟨n, le_rfl, h⟩
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (15)
Lean names referenced from this declaration's body.
-
inBall
in IndisputableMonolith.Causality.Basic
decl_use
-
Kinematics
in IndisputableMonolith.Causality.Basic
decl_use
-
ReachN
in IndisputableMonolith.Causality.Basic
decl_use
-
Kinematics
in IndisputableMonolith.Causality.ConeBound
decl_use
-
inBall
in IndisputableMonolith.Causality.Reach
decl_use
-
Kinematics
in IndisputableMonolith.Causality.Reach
decl_use
-
reach_in_ball
in IndisputableMonolith.Causality.Reach
decl_use
-
ReachN
in IndisputableMonolith.Causality.Reach
decl_use
-
K
in IndisputableMonolith.Constants
decl_use
-
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
inBall
in IndisputableMonolith.LedgerUniqueness
decl_use
-
Kinematics
in IndisputableMonolith.LedgerUniqueness
decl_use
-
ReachN
in IndisputableMonolith.LedgerUniqueness
decl_use
-
Kinematics
in IndisputableMonolith.LightCone.StepBounds
decl_use
-
ReachN
in IndisputableMonolith.LightCone.StepBounds
decl_use