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)
29noncomputable def universal_forcing (R S : LogicRealization) :
30 (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
proof body
Definition body.
31 ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
32
33/-- Peano surface is available for every realization's forced arithmetic. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
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
-
LogicRealization
in IndisputableMonolith.Foundation.LogicRealization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
arithmeticOf
in IndisputableMonolith.Foundation.UniversalForcing
decl_use
-
universal_forcing
in IndisputableMonolith.Foundation.UniversalForcing
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
universal_forcing
in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use