lemma proved term proof

`coe_mk`

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

formal statement (Lean)

  47@[simp] lemma coe_mk (f : ℝ → ℝ) (hc : ContinuousOn f (Icc a b))
  48    (hp : ∀ t ∈ Icc a b, 0 < f t) :
  49    (⟨f, hc, hp⟩ : AdmissiblePath a b).toFun = f := rfl

proof body

Term-mode proof.

  50
  51/-- The constant path at value `c > 0`. -/

depends on (3)

Lean names referenced from this declaration's body.

AdmissiblePath in IndisputableMonolith.Action.PathSpace decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use