`eventCompose_left_id`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
domain: Foundation
line: 124 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts on GitHub at line 124.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 121  · exact Nat.add_assoc _ _ _
 122  · exact Nat.add_assoc _ _ _
 123
 124theorem eventCompose_left_id (a : EventState) :
 125    eventCompose narrativeZero a = a := by
 126  unfold eventCompose narrativeZero
 127  cases a; simp
 128
 129end NarrativeRich
 130
 131/-! ## Ethics -/
 132
 133namespace EthicsRich
 134
 135open Ethics
 136
 137theorem actionCost_zero_iff (a b : ActionState) :
 138    actionCost a b = 0 ↔ a = b := by
 139  unfold actionCost
 140  by_cases h : a = b
 141  · simp [h]
 142  · simp [h]
 143
 144def actionCost_decidable (a b : ActionState) : Decidable (a = b) :=
 145  inferInstance
 146
 147theorem preferenceCompose_assoc (a b c : ActionState) :
 148    preferenceCompose (preferenceCompose a b) c =
 149    preferenceCompose a (preferenceCompose b c) := by
 150  unfold preferenceCompose
 151  congr 1
 152  exact Nat.add_assoc _ _ _
 153
 154theorem preferenceCompose_left_id (a : ActionState) :

papers checked against this theorem

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