pith. machine review for the scientific record. sign in
def definition def or abbrev

IsCoarseGrainingStable

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  78def IsCoarseGrainingStable (c : CohomologyClass) : Prop :=

proof body

Definition body.

  79  True
  80
  81/-! ## J-Cost Minimal Sub-Ledgers (Algebraic Cycles) -/
  82
  83/-- A sub-ledger is J-cost minimal if no proper sub-sub-ledger has lower
  84    total defect. These are the recognition-closed subgraphs. -/

used by (4)

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

depends on (18)

Lean names referenced from this declaration's body.