theorem proved term proof

`recognition_implies_existence`

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

formal statement (Lean)

  45theorem recognition_implies_existence {X : Type*}
  46    (h : ∃ (R : X → X → Prop), ∃ x, R x x) : Nonempty X :=

Term-mode proof.

  47  MetaPrinciple X h
  48
  49/-- The contrapositive: emptiness implies no self-recognition. -/

Lean names referenced from this declaration's body.