`all`

definition

show as: view math explainer →

module: IndisputableMonolith.Aesthetics.NarrativeGeodesic
domain: Aesthetics
line: 113 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Aesthetics.NarrativeGeodesic on GitHub at line 113.

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

 110  | rebirth              => "Rebirth"
 111
 112/-- The seven-element list of plot families. -/
 113def all : List BookerPlotFamily :=
 114  [overcomingTheMonster, ragsToRiches, theQuest, voyageAndReturn,
 115   comedy, tragedy, rebirth]
 116
 117/-- The list has length 7. -/
 118theorem all_length : all.length = 7 := by
 119  unfold all; decide
 120
 121/-- The list is nodup. -/
 122theorem all_nodup : all.Nodup := by
 123  unfold all; decide
 124
 125instance : Fintype BookerPlotFamily where
 126  elems := { val := ⟦all⟧, nodup := all_nodup }
 127  complete := by
 128    intro x; cases x <;> decide
 129
 130/-- `BookerPlotFamily` has exactly seven elements. -/
 131theorem card_eq_seven : Fintype.card BookerPlotFamily = 7 := by
 132  rfl
 133
 134end BookerPlotFamily
 135
 136/-! ## §2. The bijection with `F2Power 3 \ {0}` -/
 137
 138/-- The explicit axis encoding of the seven plot families per
 139    Theorem 9 of `Seven_Plots_Three_Dimensions.tex`. The three
 140    axes are protagonist status (axis 1), world status (axis 2),
 141    and value alignment (axis 3). -/
 142def plotEncoding : BookerPlotFamily → F2Power 3
 143  | .ragsToRiches         => axis1     -- (true, false, false)

papers checked against this theorem

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