join_cons — Mathlib

English

Join distributes over a constructor: join ((a, Seq.cons b s), S) = (a, Seq.join (Seq.cons (b, s) S)).

Русский

Образование объединения через join распределяется над конструктором: join ((a, Seq.cons b s), S) = (a, Seq.join (Seq.cons (b, s) S)).

LaTeX

$$$\\operatorname{join}((a, \\mathrm{Seq.cons}\\; b\\; s), S) = (a, \\mathrm{Seq.join}(\\mathrm{Seq.cons}(b, s)\\; S))$$$

Lean4

@[simp]
theorem join_cons (a b : α) (s S) : join ((a, Seq.cons b s), S) = (a, Seq.join (Seq.cons (b, s) S)) := by dsimp [join];
  rw [destruct_cons]

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