`cert`

definition

show as: view math explainer →

module: IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
domain: GameTheory
line: 73 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim on GitHub at line 73.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  70  mwc_le_half : 2 * mwcSize ≤ totalCoalitionTypes + 1
  71  mwc_pos : 0 < mwcSize
  72
  73noncomputable def cert : CoalitionSizeCert where
  74  total_eq := totalCoalitionTypes_eq
  75  mwc_eq := mwcSize_eq
  76  mwc_le_half := mwcSize_le_half
  77  mwc_pos := mwcSize_pos
  78
  79theorem cert_inhabited : Nonempty CoalitionSizeCert := ⟨cert⟩
  80
  81end
  82end CoalitionSizeFromConfigDim
  83end GameTheory
  84end IndisputableMonolith

papers checked against this theorem

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