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

clusteringRatio_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)

  89theorem clusteringRatio_lt_one : clusteringRatio < 1 := by

proof body

Term-mode proof.

  90  unfold clusteringRatio
  91  rw [div_lt_one phi_pos]
  92  exact one_lt_phi
  93

depends on (4)

Lean names referenced from this declaration's body.