theorem proved term proof

`MetaPrinciple`

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

formal statement (Lean)

  39theorem MetaPrinciple (X : Type*) :
  40    (∃ (R : X → X → Prop), ∃ x, R x x) → Nonempty X := by

Term-mode proof.

  41  intro ⟨_, x, _⟩
  42  exact ⟨x⟩
  43
  44/-- Constructive version: recognition implies existence. -/

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

recognition_implies_existence in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use
recognition_structure_nonempty in IndisputableMonolith.RRF.Foundation.MetaPrinciple decl_use