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

interp_fixedEndpoints

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)

 151lemma interp_fixedEndpoints {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
 152    (h : fixedEndpoints γ₁ γ₂) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
 153    fixedEndpoints γ₁ (interp γ₁ γ₂ s hs) := by

proof body

Term-mode proof.

 154  refine ⟨?_, ?_⟩
 155  · simp [interp_apply, h.1]; ring
 156  · simp [interp_apply, h.2]; ring
 157
 158/-! ## Status report -/
 159
 160/-- Status string for the path-space module. -/

depends on (6)

Lean names referenced from this declaration's body.