inductive
definition
MeasurementLevel
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.MeasurementTheoryFromRS on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
19
20namespace IndisputableMonolith.Physics.MeasurementTheoryFromRS
21
22inductive MeasurementLevel where
23 | nominal | ordinal | interval | ratio | absolute
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem measurementLevelCount : Fintype.card MeasurementLevel = 5 := by decide
27
28structure MeasurementTheoryCert where
29 five_levels : Fintype.card MeasurementLevel = 5
30
31def measurementTheoryCert : MeasurementTheoryCert where
32 five_levels := measurementLevelCount
33
34end IndisputableMonolith.Physics.MeasurementTheoryFromRS