English
A more explicit formulation of image2_image2_image2_comm with additional variable bindings; equality holds under a universal distributivity condition h_comm.
Русский
Уточнённое формулирование для image2_image2_image2_comm при дополнительных переменных; равенство выполняется при условии общности равенств распределения.
LaTeX
$$$\\forall a b c d,\\, f(g(a,b), h(c,d)) = f'(g'(a,c), h'(b,d)) \\Rightarrow \\operatorname{image}_2 f (\\operatorname{image}_2 g s t) (\\operatorname{image}_2 h u v) = \\operatorname{image}_2 f' (\\operatorname{image}_2 g' s u) (\\operatorname{image}_2 h' t v)$$$
Lean4
theorem image2_image2_image2_comm {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ} {f' : ε' → ζ' → ν} {g' : α → γ → ε'}
{h' : β → δ → ζ'} (h_comm : ∀ a b c d, f (g a b) (h c d) = f' (g' a c) (h' b d)) :
image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v) := by grind
