seq_seq — Mathlib

English

The associativity of the seq operation: s.seq(t.seq(u)) equals seq of seq composition applied to s and t then u.

Русский

Ассоциативность операции seq: s.seq(t.seq(u)) = seq((∘)''s ∘ t) u.

LaTeX

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

Lean4

theorem seq_seq {s : Set (β → γ)} {t : Set (α → β)} {u : Set α} : seq s (seq t u) = seq (seq ((· ∘ ·) '' s) t) u :=
  by
  simp only [seq_eq_image2, image2_image_left]
  exact .symm <| image2_assoc fun _ _ _ ↦ rfl

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