def
definition
name
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Aesthetics.NarrativeGeodesic on GitHub at line 103.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
100namespace BookerPlotFamily
101
102/-- A short name for display. -/
103def name : BookerPlotFamily → String
104 | overcomingTheMonster => "Overcoming the Monster"
105 | ragsToRiches => "Rags to Riches"
106 | theQuest => "The Quest"
107 | voyageAndReturn => "Voyage and Return"
108 | comedy => "Comedy"
109 | tragedy => "Tragedy"
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