Zulip Chat Archive
Stream: general
Topic: why is image_add_const_Ici backwards?
Scott Morrison (Apr 20 2021 at 08:08):
It seems image_add_const_Ici and its relatives have a gratuitous reversal of the addition. Does anyone know why?
@[simp] lemma image_add_const_Ici : (λ x, x + a) '' Ici b = Ici (a + b) := by simp [add_comm]
Yury G. Kudryashov (Jun 19 2021 at 20:17):
I don't remember why I did this. Feel free to change (if not changed yet).
Last updated: May 02 2025 at 03:31 UTC