theorem proved term proof

`strict_peano_surface`

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

formal statement (Lean)

  33theorem strict_peano_surface (R : StrictLogicRealization) :
  34    ArithmeticOf.PeanoSurface (StrictLogicRealization.arith R) :=

proof body

Term-mode proof.

  35  StrictLogicRealization.peano_surface R
  36
  37end Invariance
  38end Strict
  39end UniversalForcing
  40end Foundation
  41end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.

ArithmeticOf in IndisputableMonolith.Foundation.ArithmeticOf decl_use
PeanoSurface in IndisputableMonolith.Foundation.ArithmeticOf decl_use
peano_surface in IndisputableMonolith.Foundation.UniversalForcing decl_use
arith in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
peano_surface in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
StrictLogicRealization in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use