`essFromSigmaCert`

definition

show as: view math explainer →

module: IndisputableMonolith.GameTheory.ESSFromSigma
domain: GameTheory
line: 75 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.GameTheory.ESSFromSigma on GitHub at line 75.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  72  no_coop_not_isESS : ¬ isESS 0
  73
  74/-- The master certificate is inhabited. -/
  75def essFromSigmaCert : ESSFromSigmaCert where
  76  threshold_pos := cooperatorThreshold_pos
  77  threshold_lt_one := cooperatorThreshold_lt_one
  78  all_coop_isESS := all_cooperator_isESS
  79  no_coop_not_isESS := no_cooperator_not_isESS
  80
  81end
  82
  83end ESSFromSigma
  84end GameTheory
  85end IndisputableMonolith

papers checked against this theorem

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