inductive
definition
OceanLayer
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.OceanographyFromRS 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.OceanographyFromRS
21
22inductive OceanLayer where
23 | surface | thermocline | intermediate | deep | abyssal
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem oceanLayerCount : Fintype.card OceanLayer = 5 := by decide
27
28structure OceanographyCert where
29 five_layers : Fintype.card OceanLayer = 5
30
31def oceanographyCert : OceanographyCert where
32 five_layers := oceanLayerCount
33
34end IndisputableMonolith.Physics.OceanographyFromRS