def definition def or abbrev

`IsSeparating`

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

formal statement (Lean)

  42def IsSeparating (r : Recognizer C E) : Prop :=

Definition body.

  43  Function.Injective r.R
  44
  45/-- A recognizer separates iff no two distinct configs are indistinguishable. -/

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

dimension_status in IndisputableMonolith.RecogGeom.Dimension decl_use
independent_strict_refines in IndisputableMonolith.RecogGeom.Dimension decl_use
isSeparating_iff in IndisputableMonolith.RecogGeom.Dimension decl_use
PairSeparates in IndisputableMonolith.RecogGeom.Dimension decl_use
pairSeparates_iff in IndisputableMonolith.RecogGeom.Dimension decl_use
separating_quotient_bijective in IndisputableMonolith.RecogGeom.Dimension decl_use
separating_singleton_cells in IndisputableMonolith.RecogGeom.Dimension decl_use

Lean names referenced from this declaration's body.