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

realizationLift

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)

 134def realizationLift (R : LogicRealization) (B : PeanoObject) :
 135    PeanoObject.Hom (realizationPeano R) B where
 136  toFun := realizationFold R B

proof body

Definition body.

 137  map_zero := by
 138    unfold realizationFold
 139    change (logicNatLift B).toFun (R.orbitEquivLogicNat R.orbitZero) = B.zero
 140    rw [R.orbitEquiv_zero]
 141    rfl
 142  map_step := by
 143    intro x
 144    unfold realizationFold
 145    change (logicNatLift B).toFun (R.orbitEquivLogicNat (R.orbitStep x)) =
 146      B.step ((logicNatLift B).toFun (R.orbitEquivLogicNat x))
 147    rw [R.orbitEquiv_step]
 148    rfl
 149

used by (2)

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.