def definition def or abbrev

`interfaceSetoid`

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

formal statement (Lean)

  48def interfaceSetoid {K : Type*} (I : PrimitiveInterface K) : Setoid K where
  49  r := I.kernel

proof body

Definition body.

  50  iseqv := kernel_is_equivalence I
  51
  52/-- The **recognition lattice** generated by an interface: the quotient by
  53the interface kernel. -/

used by (2)

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

cellOf in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use
RecognitionLattice in IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer decl_use

depends on (6)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
kernel_is_equivalence in IndisputableMonolith.Foundation.ObserverFromRecognition decl_use
PrimitiveInterface in IndisputableMonolith.Foundation.ObserverFromRecognition decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use