English
The graph on the product of sets with a product map corresponds to the preimage of the product graph under a natural rearrangement equivalence.
Русский
Граф на произведении множеств с отображением в произведение соответствует предобразу графа на произведение под естественным эквивалентным преобразованием переупорядочивания.
LaTeX
$$$(s \times^{\mathrm{⋯}} t).graphOn (Prod.map f g) = \text{preimage} (EquivLike.toFunLike.coe (Equiv.prodProdProdComm α γ β δ)) (s.graphOn f \times^{\mathrm{⋯}} t.graphOn g)$$$
Lean4
theorem graphOn_prod_graphOn (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
s.graphOn f ×ˢ t.graphOn g = Equiv.prodProdProdComm .. ⁻¹' (s ×ˢ t).graphOn (Prod.map f g) := by aesop
