def definition def or abbrev

`mapUncertainty`

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

formal statement (Lean)

 145def mapUncertainty {α : Type} (uMap : Uncertainty → Uncertainty) (m : Measurement α) : Measurement α :=

proof body

Definition body.

 146  { value := m.value
 147    window := m.window
 148    protocol := m.protocol
 149    uncertainty := m.uncertainty.map uMap
 150    notes := m.notes
 151  }
 152

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

measure_to_joules in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use
measure_to_joule_seconds in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use
measure_to_meters in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use
measure_to_seconds in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use

depends on (6)

Lean names referenced from this declaration's body.

Measurement in IndisputableMonolith.Data.Import decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
Uncertainty in IndisputableMonolith.Measurement.RSNative.Core decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use