module module

`IndisputableMonolith.CrossDomain.PlanetStratification`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

declarations in this module (14)

inductive AtmosphericLayer L25
inductive EarthLayer L29
inductive OceanLayer L33
theorem atmoCount L37
theorem earthCount L38
theorem oceanCount L39
abbrev PlanetStratum L41
theorem planetStratumCount L43
theorem atmo_is_proper_subset L47
theorem earth_is_proper_subset L51
theorem ocean_is_proper_subset L55
theorem planetStratum_three_D L60
structure PlanetStratificationCert L62
def planetStratificationCert L69