structure
definition
PlanetStratificationCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CrossDomain.PlanetStratification on GitHub at line 62.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
59/-- 15 = 3 × D (where D = 5). -/
60theorem planetStratum_three_D : 15 = 3 * 5 := by decide
61
62structure PlanetStratificationCert where
63 stratum_count : Fintype.card PlanetStratum = 15
64 three_D : 15 = 3 * 5
65 atmo_sub : Fintype.card PlanetStratum > Fintype.card AtmosphericLayer
66 earth_sub : Fintype.card PlanetStratum > Fintype.card EarthLayer
67 ocean_sub : Fintype.card PlanetStratum > Fintype.card OceanLayer
68
69def planetStratificationCert : PlanetStratificationCert where
70 stratum_count := planetStratumCount
71 three_D := planetStratum_three_D
72 atmo_sub := atmo_is_proper_subset
73 earth_sub := earth_is_proper_subset
74 ocean_sub := ocean_is_proper_subset
75
76end IndisputableMonolith.CrossDomain.PlanetStratification