theorem proved term proof

`bool_peano_surface`

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

formal statement (Lean)

  78theorem bool_peano_surface :
  79    ArithmeticOf.PeanoSurface (UniversalForcing.arithmeticOf boolRealization) :=

Term-mode proof.

  80  UniversalForcing.peano_surface boolRealization
  81
  82end DiscreteLogicRealization
  83end Foundation
  84end IndisputableMonolith

Lean names referenced from this declaration's body.

ArithmeticOf in IndisputableMonolith.Foundation.ArithmeticOf decl_use
PeanoSurface in IndisputableMonolith.Foundation.ArithmeticOf decl_use
boolRealization in IndisputableMonolith.Foundation.DiscreteLogicRealization decl_use
arithmeticOf in IndisputableMonolith.Foundation.UniversalForcing decl_use
peano_surface in IndisputableMonolith.Foundation.UniversalForcing decl_use
peano_surface in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use