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

continuous_positive_ratio_arithmetic_invariant

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)

  50noncomputable def continuous_positive_ratio_arithmetic_invariant
  51    (C : LogicAsFunctionalEquation.ComparisonOperator)
  52    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C)
  53    (S : LogicRealization.{0, 0}) :
  54    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier
  55      ≃ (arithmeticOf S).peano.carrier :=

proof body

Definition body.

  56  ArithmeticOf.equivOfInitial
  57    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)) (arithmeticOf S)
  58
  59/-- The Peano surface is available for the forced arithmetic of every
  60realization. -/

depends on (20)

Lean names referenced from this declaration's body.