graphOn_prod_prodMap — Mathlib

English

The graph on the product with map Prod.map f g equals the preimage under a natural equivalence of the product graphs on f and g.

Русский

Граф на произведении с отображением Prod.map f g равен предобразу под естественным эквивалентным преобразованием графов f и g.

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_prodMap (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
    (s ×ˢ t).graphOn (Prod.map f g) = Equiv.prodProdProdComm .. ⁻¹' s.graphOn f ×ˢ t.graphOn g := by aesop

Похожие утверждения