image2_eq_seq — Mathlib

English

The image of s × t under the prod mk mapping equals the sequence of the set image of s under the function that maps b to (a,b) and t.

Русский

Образ множества s × t под отображением Prod.mk равен последовательности образов множества s под отображением, переводящим b в (a,b).

LaTeX

$$$$ \\operatorname{image}_2 f s t = \\operatorname{seq} (f'' s) t $$$$

Lean4

theorem image2_eq_seq (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = seq (f '' s) t := by
  rw [seq_eq_image2, image2_image_left]

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