  22
  23namespace IndisputableMonolith.CrossDomain.PlanetStratification
  24
  25inductive AtmosphericLayer where
  26  | troposphere | stratosphere | mesosphere | thermosphere | exosphere
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29inductive EarthLayer where
  30  | innerCore | outerCore | lowerMantle | upperMantle | crust
  31  deriving DecidableEq, Repr, BEq, Fintype
  32
  33inductive OceanLayer where
  34  | surface | thermocline | intermediate | deep | abyssal
  35  deriving DecidableEq, Repr, BEq, Fintype
  36
  37theorem atmoCount : Fintype.card AtmosphericLayer = 5 := by decide
  38theorem earthCount : Fintype.card EarthLayer = 5 := by decide
  39theorem oceanCount : Fintype.card OceanLayer = 5 := by decide
  40
  41abbrev PlanetStratum : Type := AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer
  42
  43theorem planetStratumCount : Fintype.card PlanetStratum = 15 := by
  44  simp only [PlanetStratum, Fintype.card_sum, atmoCount, earthCount, oceanCount]
  45
  46/-- The three injections are not surjective: each covers only 5 of 15. -/
  47theorem atmo_is_proper_subset :
  48    Fintype.card PlanetStratum > Fintype.card AtmosphericLayer := by
  49  rw [planetStratumCount, atmoCount]; decide
  50
  51theorem earth_is_proper_subset :
  52    Fintype.card PlanetStratum > Fintype.card EarthLayer := by
  53  rw [planetStratumCount, earthCount]; decide
  54
  55theorem ocean_is_proper_subset :

papers checked against this theorem

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