`_ordered_ok`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit
domain: Foundation
line: 51 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.AxiomAudit on GitHub at line 51.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  48
  49/-! ## Strict mathematical realizations -/
  50
  51def _ordered_ok :
  52    (StrictLogicRealization.arith strictOrderedRealization).peano.carrier
  53      ≃ ArithmeticFromLogic.LogicNat :=
  54  (StrictLogicRealization.toLightweight strictOrderedRealization).orbitEquivLogicNat
  55
  56def _categorical_ok :
  57    (StrictLogicRealization.arith strictCategoricalRealization).peano.carrier
  58      ≃ ArithmeticFromLogic.LogicNat :=
  59  (StrictLogicRealization.toLightweight strictCategoricalRealization).orbitEquivLogicNat
  60
  61/-! ## Strict domain realizations -/
  62
  63noncomputable def _music_ok :
  64    (StrictLogicRealization.arith strictMusicRealization).peano.carrier
  65      ≃ ArithmeticFromLogic.LogicNat :=
  66  (StrictLogicRealization.toLightweight strictMusicRealization).orbitEquivLogicNat
  67
  68def _biology_ok :
  69    (StrictLogicRealization.arith strictBiologyRealization).peano.carrier
  70      ≃ ArithmeticFromLogic.LogicNat :=
  71  (StrictLogicRealization.toLightweight strictBiologyRealization).orbitEquivLogicNat
  72
  73def _narrative_ok :
  74    (StrictLogicRealization.arith strictNarrativeRealization).peano.carrier
  75      ≃ ArithmeticFromLogic.LogicNat :=
  76  (StrictLogicRealization.toLightweight strictNarrativeRealization).orbitEquivLogicNat
  77
  78def _ethics_ok :
  79    (StrictLogicRealization.arith strictEthicsRealization).peano.carrier
  80      ≃ ArithmeticFromLogic.LogicNat :=
  81  (StrictLogicRealization.toLightweight strictEthicsRealization).orbitEquivLogicNat

papers checked against this theorem

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