def definition def or abbrev

`cellLabel`

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

formal statement (Lean)

  72def cellLabel {K : Type*} (I : PrimitiveInterface K) :
  73    RecognitionLattice I → Fin I.n :=

Definition body.

  74  Quotient.lift (fun x => I.observe x) (by
  75    intro x y h
  76    exact h)
  77

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

cellLabel_cellOf in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use
every_cell_has_label in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use
neighborhood in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
PrimitiveInterface in IndisputableMonolith.Foundation.ObserverFromRecognition decl_use
RecognitionLattice in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use