def definition def or abbrev

`essFromSigmaCert`

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

formal statement (Lean)

  75def essFromSigmaCert : ESSFromSigmaCert where
  76  threshold_pos := cooperatorThreshold_pos

proof body

Definition body.

  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

depends on (5)

Lean names referenced from this declaration's body.

all_cooperator_isESS in IndisputableMonolith.GameTheory.ESSFromSigma decl_use
cooperatorThreshold_lt_one in IndisputableMonolith.GameTheory.ESSFromSigma decl_use
cooperatorThreshold_pos in IndisputableMonolith.GameTheory.ESSFromSigma decl_use
ESSFromSigmaCert in IndisputableMonolith.GameTheory.ESSFromSigma decl_use
no_cooperator_not_isESS in IndisputableMonolith.GameTheory.ESSFromSigma decl_use