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

empty_has_no_self_recognition

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)

  50theorem empty_has_no_self_recognition (X : Type*) (h : IsEmpty X) :
  51    ¬(∃ (R : X → X → Prop), ∃ x, R x x) := by

proof body

Term-mode proof.

  52  intro ⟨_, x, _⟩
  53  exact h.elim x
  54
  55/-! ## Recognition Structure -/
  56
  57/-- A recognition structure on a type.
  58
  59This captures the minimal structure needed for "things to be recognized."
  60-/

depends on (5)

Lean names referenced from this declaration's body.