structure definition def or abbrev

`Recognizer`

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

formal statement (Lean)

  34structure Recognizer (C : Type*) (E : Type*) where
  35  /-- The recognition function mapping configurations to events -/
  36  R : C → E
  37  /-- The recognizer is nontrivial: at least two distinct events are produced -/
  38  nontrivial : ∃ c₁ c₂ : C, R c₁ ≠ R c₂
  39
  40/-- A local recognizer is a recognizer on a local configuration space -/

depends on (40)

Lean names referenced from this declaration's body.

nontrivial in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
nontrivial in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
nontrivial in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Structure in IndisputableMonolith.Chemistry.CrystalStructure decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
neighborhood in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use

… and 10 more