Stream: Beginner Questions

Topic: Associativity Map Composition

Robert Soeldner (Dec 04 2021 at 07:58):

I was not able to find a lemma corresponding to the associativity law for map composition in the theory Map.
Is it missing or have I just failed to find it ?

lemma "(a ∘⇩m b) ∘⇩m c = a ∘⇩m (b ∘⇩m c)"
  unfolding map_comp_def
  by (metis option.case_eq_if)

Last updated: Feb 01 2025 at 20:19 UTC