pith. machine review for the scientific record. sign in
theorem proved term proof

aggregateThroughput_pos

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)

  62theorem aggregateThroughput_pos {N : ℕ} (h : 1 ≤ N) :
  63    0 < aggregateThroughput N := by

proof body

Term-mode proof.

  64  unfold aggregateThroughput
  65  exact mul_pos (by exact_mod_cast (by omega : 0 < N)) T_node_pos
  66

depends on (2)

Lean names referenced from this declaration's body.