`peano_surface`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
domain: Foundation
line: 110 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.StrictRealization on GitHub at line 110.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 107  ArithmeticOf.equivOfInitial (arith R) (arith S)
 108
 109/-- The Peano surface is inherited from the derived free orbit. -/
 110theorem peano_surface (R : StrictLogicRealization) :
 111    ArithmeticOf.PeanoSurface (arith R) :=
 112  UniversalForcing.peano_surface (toLightweight R)
 113
 114end StrictLogicRealization
 115
 116end Strict
 117end UniversalForcing
 118end Foundation
 119end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.