def definition def or abbrev

`narrative_arith_equiv_nat`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  70noncomputable def narrative_arith_equiv_nat :
  71    (arithmeticOf narrativeRealization).peano.carrier ≃ LogicNat :=

proof body

Definition body.

  72  narrativeRealization.orbitEquivLogicNat
  73
  74end NarrativeRealization
  75end UniversalForcing
  76end Foundation
  77end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
arithmeticOf in IndisputableMonolith.Foundation.UniversalForcing decl_use
narrativeRealization in IndisputableMonolith.Foundation.UniversalForcing.NarrativeRealization decl_use