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)
22inductive EarthLayer where
23 | innerCore | outerCore | lowerMantle | upperMantle | crust
24 deriving DecidableEq, Repr, BEq, Fintype
25
used by (10)
From the project-wide theorem graph. These declarations reference this one in their body.
-
earthCount
in IndisputableMonolith.CrossDomain.PlanetStratification
decl_use
-
earth_is_proper_subset
in IndisputableMonolith.CrossDomain.PlanetStratification
decl_use
-
EarthLayer
in IndisputableMonolith.CrossDomain.PlanetStratification
decl_use
-
PlanetStratificationCert
in IndisputableMonolith.CrossDomain.PlanetStratification
decl_use
-
PlanetStratum
in IndisputableMonolith.CrossDomain.PlanetStratification
decl_use
-
earthLayerCount
in IndisputableMonolith.Physics.GeophysicsFromRS
decl_use
-
GeophysicsCert
in IndisputableMonolith.Physics.GeophysicsFromRS
decl_use
-
earthAxis
in IndisputableMonolith.Physics.PlanetStrataC2
decl_use
-
PlanetStrataCert
in IndisputableMonolith.Physics.PlanetStrataC2
decl_use
-
planet_strata_total_15
in IndisputableMonolith.Physics.PlanetStrataC2
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
EarthLayer
in IndisputableMonolith.CrossDomain.PlanetStratification
decl_use