image_seq — Mathlib

English

The image of the seq of s under t equals the seq of the image of s under f, namely f shows up in the outer image.

Русский

Образ последовательности наборов через seq равен последовательности образов.

LaTeX

$$$$ f'' \\operatorname{seq} s t = \\operatorname{seq} ((f \\circ \\cdot) '' s) t $$$$

Lean4

theorem image_seq {f : β → γ} {s : Set (α → β)} {t : Set α} : f '' seq s t = seq ((f ∘ ·) '' s) t := by
  simp only [seq, image_image2, image2_image_left, comp_apply]

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