pith. machine review for the scientific record. sign in
def definition def or abbrev

styleSuccessionCert

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  97def styleSuccessionCert : StyleSuccessionCert where
  98  canon_length := westernCanon_length

proof body

Definition body.

  99  average_gap_eq := averageGap_eq
 100  average_gap_in_band := averageGap_in_gap45_band
 101  average_above_gap45 := averageGap_above_gap45
 102  gap45_eq := rfl
 103
 104/-- **ART HISTORY ONE-STATEMENT.** Western canon has 11 named styles
 105spanning 1400–1960; average inter-style gap = 56 yr, in the gap-45
 106band `[15, 90]`. -/

depends on (14)

Lean names referenced from this declaration's body.