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

measure_to_seconds

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)

  53noncomputable def measure_to_seconds (cal : ExternalCalibration) (m : Measurement Tick) : Measurement ℝ :=

proof body

Definition body.

  54  Measurement.map (to_seconds cal)
  55    (Measurement.mapUncertainty
  56      (fun u => scaleUncertainty cal.seconds_per_tick (le_of_lt cal.seconds_pos) u) m)
  57

depends on (13)

Lean names referenced from this declaration's body.