theorem
proved
T3_continuity
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Chain on GitHub at line 55.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
52 have hv' : v = w := huniq v hv
53 exact hu'.trans hv'.symm
54
55theorem T3_continuity {M} (L : Ledger M) [Conserves L] :
56 ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0 := Conserves.conserve
57
58end IndisputableMonolith