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

distinction_realizations_have_same_arithmetic

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)

 178noncomputable def distinction_realizations_have_same_arithmetic
 179    {K L : Type u} [DecidableEq K] [DecidableEq L]
 180    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
 181    (UniversalForcing.arithmeticOf
 182      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃
 183    (UniversalForcing.arithmeticOf
 184      (logicRealizationOfDistinction L a b hab)).peano.carrier :=

proof body

Definition body.

 185  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat.trans
 186    (logicRealizationOfDistinction L a b hab).orbitEquivLogicNat.symm
 187
 188/-! ## Certificate -/
 189

depends on (8)

Lean names referenced from this declaration's body.