lemma proved term proof

`fixedEndpoints_symm`

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

formal statement (Lean)

  97lemma fixedEndpoints_symm {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
  98    (h : fixedEndpoints γ₁ γ₂) : fixedEndpoints γ₂ γ₁ :=

Term-mode proof.

  99  ⟨h.1.symm, h.2.symm⟩
 100

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

actionJ_minimum_unique_value in IndisputableMonolith.Action.FunctionalConvexity decl_use

Lean names referenced from this declaration's body.