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)
130def realizationFold (R : LogicRealization) (B : PeanoObject) : R.Orbit → B.carrier :=
proof body
Definition body.
131 fun n => (logicNatLift B).toFun (R.orbitEquivLogicNat n)
132
133/-- Homomorphism from the extracted realization orbit into any Peano object. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (7)
Lean names referenced from this declaration's body.
-
carrier
in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice
decl_use
-
carrier
in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity
decl_use
-
extracted
in IndisputableMonolith.Foundation.ArithmeticOf
decl_use
-
logicNatLift
in IndisputableMonolith.Foundation.ArithmeticOf
decl_use
-
PeanoObject
in IndisputableMonolith.Foundation.ArithmeticOf
decl_use
-
LogicRealization
in IndisputableMonolith.Foundation.LogicRealization
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use