def definition def or abbrev

`fixedEndpoints`

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

formal statement (Lean)

  91def fixedEndpoints {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) : Prop :=

Definition body.

  92  γ₁.toFun a = γ₂.toFun a ∧ γ₁.toFun b = γ₂.toFun b
  93

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

actionJ_minimum_unique_value in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_unconditional in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_via_convexity in IndisputableMonolith.Action.FunctionalConvexity decl_use
principle_of_least_action in IndisputableMonolith.Action.FunctionalConvexity decl_use
fixedEndpoints_refl in IndisputableMonolith.Action.PathSpace decl_use
fixedEndpoints_symm in IndisputableMonolith.Action.PathSpace decl_use
fixedEndpoints_trans in IndisputableMonolith.Action.PathSpace decl_use
interp_fixedEndpoints in IndisputableMonolith.Action.PathSpace decl_use
pathSpace_status in IndisputableMonolith.Action.PathSpace decl_use

Lean names referenced from this declaration's body.