`map`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RSNative.Core
domain: Measurement
line: 127 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.RSNative.Core on GitHub at line 127.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 124namespace Measurement
 125
 126/-- Map the value of a measurement, preserving window/protocol/uncertainty/notes. -/
 127def map {α β : Type} (f : α → β) (m : Measurement α) : Measurement β :=
 128  { value := f m.value
 129    window := m.window
 130    protocol := m.protocol
 131    uncertainty := m.uncertainty
 132    notes := m.notes
 133  }
 134
 135/-- Map the value and replace protocol (e.g., when you derive a new observable). -/
 136def mapWithProtocol {α β : Type} (f : α → β) (p : Protocol) (m : Measurement α) : Measurement β :=
 137  { value := f m.value
 138    window := m.window
 139    protocol := p
 140    uncertainty := m.uncertainty
 141    notes := m.notes
 142  }
 143
 144/-- Transform the uncertainty record (when present). -/
 145def mapUncertainty {α : Type} (uMap : Uncertainty → Uncertainty) (m : Measurement α) : Measurement α :=
 146  { value := m.value
 147    window := m.window
 148    protocol := m.protocol
 149    uncertainty := m.uncertainty.map uMap
 150    notes := m.notes
 151  }
 152
 153def addNote {α : Type} (note : String) (m : Measurement α) : Measurement α :=
 154  { m with notes := m.notes ++ [note] }
 155
 156def addNotes {α : Type} (notes : List String) (m : Measurement α) : Measurement α :=
 157  { m with notes := m.notes ++ notes }

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.