theorem
proved
compose_assoc
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts on GitHub at line 55.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
52def ratioCost_decidable (a b : FrequencyRatio) :
53 Decidable (a = b) := Classical.dec _
54
55theorem compose_assoc (a b c : FrequencyRatio) :
56 strictMusicRealization.compose (strictMusicRealization.compose a b) c =
57 strictMusicRealization.compose a (strictMusicRealization.compose b c) := by
58 show (⟨a.1 * b.1 * c.1, _⟩ : FrequencyRatio) = ⟨a.1 * (b.1 * c.1), _⟩
59 apply Subtype.ext
60 ring
61
62theorem compose_left_id (a : FrequencyRatio) :
63 strictMusicRealization.compose strictMusicRealization.one a = a := by
64 show (⟨1 * a.1, _⟩ : FrequencyRatio) = a
65 apply Subtype.ext
66 simp
67
68end MusicRich
69
70/-! ## Biology -/
71
72namespace BiologyRich
73
74open Biology
75
76theorem lineageCost_zero_iff (a b : LineageState) :
77 lineageCost a b = 0 ↔ a = b := by
78 unfold lineageCost
79 by_cases h : a = b
80 · simp [h]
81 · simp [h]
82
83def lineageCost_decidable (a b : LineageState) : Decidable (a = b) :=
84 inferInstance
85