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

arith_continuous_equiv_arith_discrete

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)

  24noncomputable def arith_continuous_equiv_arith_discrete
  25    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  26    (arithmeticOf (continuousRealization C h)).peano.carrier
  27      ≃ (arithmeticOf discreteRealization).peano.carrier :=

proof body

Definition body.

  28  ArithmeticOf.equivOfInitial (arithmeticOf (continuousRealization C h))
  29    (arithmeticOf discreteRealization)
  30
  31end TwoCases
  32end Invariance
  33end UniversalForcing
  34end Foundation
  35end IndisputableMonolith

depends on (9)

Lean names referenced from this declaration's body.