`planetStratificationCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.PlanetStratification
domain: CrossDomain
line: 69 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.PlanetStratification on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.