`strictPositiveRatio_arith_equiv_strictBoolean`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean
domain: Foundation
line: 60 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean on GitHub at line 60.

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

  57
  58/-- First strict cross-realization invariance theorem:
  59positive ratios and Boolean propositions force the same arithmetic. -/
  60noncomputable def strictPositiveRatio_arith_equiv_strictBoolean
  61    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  62    (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h)).peano.carrier
  63      ≃ (StrictLogicRealization.arith strictBooleanRealization).peano.carrier :=
  64  ArithmeticOf.equivOfInitial
  65    (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h))
  66    (StrictLogicRealization.arith strictBooleanRealization)
  67
  68end DiscreteBoolean
  69end Strict
  70end UniversalForcing
  71end Foundation
  72end IndisputableMonolith

papers checked against this theorem

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