join_cons — Mathlib

English

For any s and S, join (cons s S) = think (append s (join S)).

Русский

Для любых s,S: соединение (cons s S) равно think(append s (join S)).

LaTeX

$$$$\operatorname{join}(\operatorname{cons}(s,S)) = \operatorname{think}(\operatorname{append}(s, \operatorname{join}(S))).$$$$

Lean4

@[simp]
theorem join_cons (s : WSeq α) (S) : join (cons s S) = think (append s (join S)) :=
  by
  simp only [join, think]
  dsimp only [(· <$> ·)]
  simp [cons, append]

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