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

terminalArrow_unique_exists

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)

  66theorem terminalArrow_unique_exists (A : DistinguishedCarrier) :
  67    ∃! f : TerminalArrow A, True := by

proof body

Term-mode proof.

  68  refine ⟨terminalArrow_exists A, trivial, ?_⟩
  69  intro g _
  70  exact terminalArrow_unique A g (terminalArrow_exists A)
  71
  72/-! ## The terminal reality object -/
  73
  74/-- The terminal reality certificate is the certificate of the minimal Bool
  75carrier. Every other distinguished carrier has a unique terminal arrow to the
  76same proposition-shaped reality object. -/

used by (1)

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

depends on (19)

Lean names referenced from this declaration's body.