theorem proved term proof

`calibration_forced_from_fixpoint`

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

formal statement (Lean)

  45theorem calibration_forced_from_fixpoint
  46    (lam : ℝ) (hlam_pos : 0 < lam) (hlam_inv : lam = lam⁻¹) :
  47    lam = 1 :=

Term-mode proof.

  48  lambda_one_is_unique_fixpoint lam hlam_pos hlam_inv
  49
  50end SubstitutivityForcing
  51end Foundation
  52end IndisputableMonolith

Lean names referenced from this declaration's body.

lambda_one_is_unique_fixpoint in IndisputableMonolith.Foundation.SubstitutivityForcing decl_use