pith. machine review for the scientific record. sign in
structure definition def or abbrev

PlanetStrataCert

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

formal statement (Lean)

  71structure PlanetStrataCert where
  72  atmospheric_count : Fintype.card AtmosphericLayer = 5
  73  earth_count : Fintype.card EarthLayer = 5
  74  ocean_count : Fintype.card OceanLayer = 5
  75  total_15 : Fintype.card AtmosphericLayer + Fintype.card EarthLayer +
  76    Fintype.card OceanLayer = 15
  77  rs_sum_15 :
  78    @Fintype.card planetStrataSum.axis1.Ix planetStrataSum.axis1.finite +
  79      @Fintype.card planetStrataSum.axis2.Ix planetStrataSum.axis2.finite +
  80      @Fintype.card planetStrataSum.axis3.Ix planetStrataSum.axis3.finite = 15
  81

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.