theorem proved term proof

`rhoBandUpper_lt_one`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  28theorem rhoBandUpper_lt_one : rhoBandUpper < 1 := by

Term-mode proof.

  29  unfold rhoBandUpper
  30  exact inv_lt_one_of_one_lt₀ one_lt_phi
  31

Lean names referenced from this declaration's body.

one_lt_phi in IndisputableMonolith.Constants decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use
rhoBandUpper in IndisputableMonolith.Unification.RecognitionBandGeometry decl_use