`arith_continuous_equiv_arith_discrete`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Invariance.TwoCases
domain: Foundation
line: 24 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Invariance.TwoCases on GitHub at line 24.

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

  21
  22/-- Continuous positive-ratio arithmetic is canonically equivalent to discrete
  23Boolean arithmetic. -/
  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 :=
  28  ArithmeticOf.equivOfInitial (arithmeticOf (continuousRealization C h))
  29    (arithmeticOf discreteRealization)
  30
  31end TwoCases
  32end Invariance
  33end UniversalForcing
  34end Foundation
  35end IndisputableMonolith

papers checked against this theorem

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