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

_ethics_ok

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)

  78def _ethics_ok :
  79    (StrictLogicRealization.arith strictEthicsRealization).peano.carrier
  80      ≃ ArithmeticFromLogic.LogicNat :=

proof body

Definition body.

  81  (StrictLogicRealization.toLightweight strictEthicsRealization).orbitEquivLogicNat
  82
  83/-! ## Strict metaphysical package -/
  84
  85noncomputable example (R : StrictLogicRealization) :
  86    (StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  87  (StrictLogicRealization.toLightweight R).orbitEquivLogicNat
  88-- #print axioms Metaphysical.strict_metaphysical_ground_unique
  89--   propext, Quot.sound
  90
  91end AxiomAudit
  92end Strict
  93end UniversalForcing
  94end Foundation
  95end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.