pith. machine review for the scientific record. sign in
lemma proved term proof

interp_zero

show as:
view Lean formalization →

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)

 141lemma interp_zero {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
 142    ∀ t, (interp γ₁ γ₂ 0 ⟨le_refl 0, by norm_num⟩).toFun t = γ₁.toFun t := by

proof body

Term-mode proof.

 143  intro t; simp [interp_apply]
 144
 145/-- Interpolation at `s = 1` is the second path. -/

depends on (8)

Lean names referenced from this declaration's body.