pith. machine review for the scientific record. sign in
def definition def or abbrev

recordProgressionCert

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)

  79def recordProgressionCert : RecordProgressionCert where
  80  gap_pos := gapAt_pos'

proof body

Definition body.

  81  one_step_ratio := gapAt_succ_ratio
  82  consecutive_ratio := consecutive_gap_ratio
  83  strictly_decreasing := gapAt_strictly_decreasing
  84
  85end
  86end RecordProgressionFit
  87end Sport
  88end IndisputableMonolith

depends on (7)

Lean names referenced from this declaration's body.