inductive
definition
EarthLayer
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.GeophysicsFromRS 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.GeophysicsFromRS
21
22inductive EarthLayer where
23 | innerCore | outerCore | lowerMantle | upperMantle | crust
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem earthLayerCount : Fintype.card EarthLayer = 5 := by decide
27
28inductive GeophysicalObservable where
29 | seismicity | gravimetry | geomagnetism | heatFlow | gpsGeodesy
30 deriving DecidableEq, Repr, BEq, Fintype
31
32theorem geophysicalObservableCount : Fintype.card GeophysicalObservable = 5 := by decide
33
34structure GeophysicsCert where
35 five_layers : Fintype.card EarthLayer = 5
36 five_observables : Fintype.card GeophysicalObservable = 5
37
38def geophysicsCert : GeophysicsCert where
39 five_layers := earthLayerCount
40 five_observables := geophysicalObservableCount
41
42end IndisputableMonolith.Physics.GeophysicsFromRS