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

neutralWindow

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)

 123def neutralWindow (e₁ e₂ e₃ e₄ : LedgerEvent) : Window8 where
 124  events := fun i =>

proof body

Definition body.

 125    match i with
 126    | ⟨0, _⟩ => e₁
 127    | ⟨1, _⟩ => e₁.conj
 128    | ⟨2, _⟩ => e₂
 129    | ⟨3, _⟩ => e₂.conj
 130    | ⟨4, _⟩ => e₃
 131    | ⟨5, _⟩ => e₃.conj
 132    | ⟨6, _⟩ => e₄
 133    | ⟨7, _⟩ => e₄.conj
 134
 135/-- **PROVED: A window of paired events is neutral.** -/

used by (2)

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

depends on (15)

Lean names referenced from this declaration's body.