`strictOrderedRealization`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.Ordered
domain: Foundation
line: 29 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.Ordered on GitHub at line 29.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  26    simp [intCost, h, h']
  27
  28/-- Strict ordered integer realization. -/
  29def strictOrderedRealization : StrictLogicRealization where
  30  Carrier := ℤ
  31  Cost := Nat
  32  zeroCost := inferInstance
  33  compare := intCost
  34  compose := fun a b => a + b
  35  one := 0
  36  generator := 1
  37  identity_law := intCost_self
  38  non_contradiction_law := intCost_symm
  39  excluded_middle_law := True
  40  composition_law := True
  41  invariance_law := True
  42  nontrivial_law := by
  43    simp [intCost]
  44
  45def strictOrdered_arith_equiv_logicNat :
  46    (StrictLogicRealization.arith strictOrderedRealization).peano.carrier
  47      ≃ ArithmeticFromLogic.LogicNat :=
  48  (StrictLogicRealization.toLightweight strictOrderedRealization).orbitEquivLogicNat
  49
  50end Ordered
  51end Strict
  52end UniversalForcing
  53end Foundation
  54end IndisputableMonolith

papers checked against this theorem

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