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

cooperatorThreshold_lt_one

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)

  44theorem cooperatorThreshold_lt_one : cooperatorThreshold < 1 := by

proof body

Tactic-mode proof.

  45  unfold cooperatorThreshold
  46  have : 1 < phi := by have := phi_gt_onePointFive; linarith
  47  rw [div_lt_one phi_pos]
  48  exact this
  49
  50/-- The threshold is strictly positive. -/

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.