`narrative_arith_equiv_nat`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.NarrativeRealization
domain: Foundation
line: 70 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.NarrativeRealization on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  67    refine ⟨1, ?_⟩
  68    simp [narrativeCost]
  69
  70noncomputable def narrative_arith_equiv_nat :
  71    (arithmeticOf narrativeRealization).peano.carrier ≃ LogicNat :=
  72  narrativeRealization.orbitEquivLogicNat
  73
  74end NarrativeRealization
  75end UniversalForcing
  76end Foundation
  77end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.