prod_image_seq_comm — Mathlib

English

The commutation between image, product, and seq operations: (Prod.mk '' s).seq t equals seq of a certain image of t with s.

Русский

Коммутативность операций образа, произведения и последовательности: (Prod.mk '' s).seq t = seq ((fun b a => (a,b)) '' t) s.

LaTeX

$$$$ (\\operatorname{Prod.mk} '' s) .\\operatorname{seq} t = \\operatorname{seq} ((\\lambda b a. (a,b)) '' t) s $$$$

Lean4

theorem prod_image_seq_comm (s : Set α) (t : Set β) : (Prod.mk '' s).seq t = seq ((fun b a => (a, b)) '' t) s := by
  rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]; rfl

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