N-ary image

Stream: maths

[Yaël Dillies]

Are those true? I doubt so, because the RHS has cross terms within the same set, but I want your opinion.

import data.set.basic

open set

variables {α β γ δ α' β' δ' : Type*} {s : set α} {t : set β} {u : set γ}

lemma image2_image2_distrib_left {f : β → γ → δ} {g : α → δ → δ'}
  {f' : β' → γ' → δ'} {g₁ : α → β → β'} {g₂ : α → γ → γ'}
  (h_distrib : ∀ a b c, g a (f b c) = f' (g₁ a b) (g₂ a c)) :
  image2 g s (image2 f t u) = image2 f' (image2 g₁ s t) (image2 g₂ s u) :=
sorry

lemma image2_image2_distrib_right {f : α → β → δ} {g : δ → γ → δ'}
  {f' : α' → β' → δ'} {g₁ : α → γ → α'} {g₂ : β → γ → β'}
  (h_distrib : ∀ a b c, g (f a b) c = f' (g₁ a c) (g₂ b c)) :
  image2 g (image2 f s t) u = image2 f' (image2 g₁ s u) (image2 g₂ t u) :=
sorry

[Yaël Dillies]

This comes up when trying to prove mul_distrib_mul_action (set α) (set β).

[Kevin Buzzard]

docs#set.image2

[Kevin Buzzard]

Surely it's not hard to make a counterexample. Make sure s has two distinct elements x and y, t and u can just have one element b and c, and then on the right hand side you have f'(g1(x,b),g2(y,c)) which you can say nothing about (so just choose g1,g2,f' arbitrary etc)