def definition def or abbrev

`strict_universal_forcing`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  26noncomputable def strict_universal_forcing (R S : StrictLogicRealization) :
  27    (StrictLogicRealization.arith R).peano.carrier
  28      ≃ (StrictLogicRealization.arith S).peano.carrier :=

proof body

Definition body.

  29  ArithmeticOf.equivOfInitial (StrictLogicRealization.arith R)
  30    (StrictLogicRealization.arith S)
  31
  32/-- The Peano surface for every strict realization. -/

depends on (8)

Lean names referenced from this declaration's body.

carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
ArithmeticOf in IndisputableMonolith.Foundation.ArithmeticOf decl_use
equivOfInitial in IndisputableMonolith.Foundation.ArithmeticOf decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
arith in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
StrictLogicRealization in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use