:: deftheorem Def20 defines pentatonic_pythagorean_scale MUSIC_S1:def 62 :
for MS being MusicSpace
for frequency being Element of MS
for b₃ being Element of 6 -tuples_on the carrier of MS holds
( b₃ = pentatonic_pythagorean_scale (MS,frequency) iff ( b₃ . 1 = frequency & b₃ . 2 = (spiral_of_fifths (MS,frequency,frequency)) . 2 & b₃ . 3 = (spiral_of_fifths (MS,frequency,frequency)) . 4 & b₃ . 4 = (spiral_of_fifths (MS,frequency,frequency)) . 1 & b₃ . 5 = (spiral_of_fifths (MS,frequency,frequency)) . 3 & b₃ . 6 = Octave (MS,frequency) ) );