structure definition def or abbrev

`AdmissiblePath`

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

formal statement (Lean)

  33structure AdmissiblePath (a b : ℝ) where
  34  /-- The underlying function. -/
  35  toFun : ℝ → ℝ
  36  /-- Continuity on the closed interval. -/
  37  cont : ContinuousOn toFun (Icc a b)
  38  /-- Strict positivity on the closed interval. -/
  39  pos : ∀ t ∈ Icc a b, 0 < toFun t
  40
  41namespace AdmissiblePath
  42
  43variable {a b : ℝ}
  44
  45instance : CoeFun (AdmissiblePath a b) (fun _ => ℝ → ℝ) := ⟨AdmissiblePath.toFun⟩

proof body

Definition body.

used by (23)

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

actionJ_convex_on_interp in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_local_min_is_global in IndisputableMonolith.Action.FunctionalConvexity decl_use
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
actionJ in IndisputableMonolith.Action.PathSpace decl_use
actionJ_const_one in IndisputableMonolith.Action.PathSpace decl_use
actionJ_def in IndisputableMonolith.Action.PathSpace decl_use
actionJ_nonneg in IndisputableMonolith.Action.PathSpace decl_use
coe_mk in IndisputableMonolith.Action.PathSpace decl_use
const in IndisputableMonolith.Action.PathSpace decl_use
const_apply in IndisputableMonolith.Action.PathSpace decl_use
fixedEndpoints in IndisputableMonolith.Action.PathSpace 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 in IndisputableMonolith.Action.PathSpace decl_use
interp_apply in IndisputableMonolith.Action.PathSpace decl_use
interp_fixedEndpoints in IndisputableMonolith.Action.PathSpace decl_use
interp_one in IndisputableMonolith.Action.PathSpace decl_use
interp_zero in IndisputableMonolith.Action.PathSpace decl_use
pathSpace_status in IndisputableMonolith.Action.PathSpace decl_use

depends on (1)

Lean names referenced from this declaration's body.

interval in IndisputableMonolith.Unification.SpacetimeEmergence decl_use