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

reverse_swaps_endpoints

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)

  44theorem reverse_swaps_endpoints :
  45    reverse ⟨0, by decide⟩ = ⟨7, by decide⟩ ∧
  46    reverse ⟨7, by decide⟩ = ⟨0, by decide⟩ := by

proof body

Term-mode proof.

  47  refine ⟨?_, ?_⟩
  48  · apply Fin.ext; simp [reverse]
  49  · apply Fin.ext; simp [reverse]
  50
  51/-- Mid-life stages invert before early ones:
  52    reverse of stage 6 (generativity) = stage 1 (autonomy),
  53    reverse of stage 0 (trust) = stage 7 (integrity).
  54    So going in reverse from old-age, we pass stage 6's inverse at
  55    position 1 before stage 0's inverse at position 7. -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.