`arith_equiv_logicNat`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
domain: Foundation
line: 100 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.StrictRealization on GitHub at line 100.

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

  97
  98/-- Every strict realization has forced arithmetic canonically equivalent to
  99`LogicNat`. -/
 100def arith_equiv_logicNat (R : StrictLogicRealization) :
 101    (arith R).peano.carrier ≃ LogicNat :=
 102  (toLightweight R).orbitEquivLogicNat
 103
 104/-- Universal forcing for strict realizations. -/
 105noncomputable def universal_forcing (R S : StrictLogicRealization) :
 106    (arith R).peano.carrier ≃ (arith S).peano.carrier :=
 107  ArithmeticOf.equivOfInitial (arith R) (arith S)
 108
 109/-- The Peano surface is inherited from the derived free orbit. -/
 110theorem peano_surface (R : StrictLogicRealization) :
 111    ArithmeticOf.PeanoSurface (arith R) :=
 112  UniversalForcing.peano_surface (toLightweight R)
 113
 114end StrictLogicRealization
 115
 116end Strict
 117end UniversalForcing
 118end Foundation
 119end IndisputableMonolith

papers checked against this theorem

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