def definition def or abbrev

`DE`

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

formal statement (Lean)

  15def DE (δ : ℤ) (p : Pot M) : Prop := ∀ {a b}, M.R a b → p b - p a = δ

Definition body.

  16
  17/-- Package the recognition relation as a kinematics. -/

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

IsAffine in IndisputableMonolith.LedgerUniqueness decl_use
diff_const_on_component in IndisputableMonolith.Potential decl_use
diff_const_on_ReachN in IndisputableMonolith.Potential decl_use
diff_in_deltaSub in IndisputableMonolith.Potential decl_use
edge_diff_invariant in IndisputableMonolith.Potential decl_use
increment_on_ReachN in IndisputableMonolith.Potential decl_use
T4_unique_on_component in IndisputableMonolith.Potential decl_use
T4_unique_on_inBall in IndisputableMonolith.Potential decl_use
T4_unique_on_reachN in IndisputableMonolith.Potential decl_use
T4_unique_up_to_const_on_component in IndisputableMonolith.Potential decl_use

Lean names referenced from this declaration's body.

as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
Pot in IndisputableMonolith.Potential decl_use
M in IndisputableMonolith.Recognition decl_use
M in IndisputableMonolith.Recognition.Cycle3 decl_use