theorem proved term proof

`comparativeEquiv_symm`

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

formal statement (Lean)

 125theorem comparativeEquiv_symm (R : ComparativeRecognizer C E) (gt_events : Set E)
 126    {c₁ c₂ : C} (h : comparativeEquiv R gt_events c₁ c₂) :
 127    comparativeEquiv R gt_events c₂ c₁ :=

proof body

Term-mode proof.

 128  ⟨h.2, h.1⟩
 129

depends on (3)

Lean names referenced from this declaration's body.

E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
comparativeEquiv in IndisputableMonolith.RecogGeom.Comparative decl_use
ComparativeRecognizer in IndisputableMonolith.RecogGeom.Comparative decl_use