theorem proved term proof

`peano_surface`

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

formal statement (Lean)

  61theorem peano_surface (R : LogicRealization) :
  62    ArithmeticOf.PeanoSurface (arithmeticOf R) :=

Term-mode proof.

  63  ArithmeticOf.extracted_peanoSurface R
  64
  65end UniversalForcing
  66end Foundation
  67end IndisputableMonolith

From the project-wide theorem graph. These declarations reference this one in their body.

bool_peano_surface in IndisputableMonolith.Foundation.DiscreteLogicRealization decl_use
universal_peano_surface in IndisputableMonolith.Foundation.UniversalForcing.Invariance.Universal decl_use
strict_peano_surface in IndisputableMonolith.Foundation.UniversalForcing.Strict.Invariance decl_use
peano_surface in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use

Lean names referenced from this declaration's body.

ArithmeticOf in IndisputableMonolith.Foundation.ArithmeticOf decl_use
extracted_peanoSurface in IndisputableMonolith.Foundation.ArithmeticOf decl_use
PeanoSurface in IndisputableMonolith.Foundation.ArithmeticOf decl_use
LogicRealization in IndisputableMonolith.Foundation.LogicRealization decl_use
arithmeticOf in IndisputableMonolith.Foundation.UniversalForcing decl_use
peano_surface in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use