join_cons_nil — Mathlib

English

Joining a stream whose head is a pair consisting of a and nil yields a stream whose head is a followed by the join of the tail.

Русский

Объединение потока, голова которого имеет вид пары (a, nil), дает поток с головой a и далее join хвоста.

LaTeX

$$$\forall a S, join (cons (a, \text{nil}) S) = cons a (join S)$$$

Lean4

theorem join_cons_nil (a : α) (S) : join (cons (a, nil) S) = cons a (join S) :=
  destruct_eq_cons <| by
    simp [join]
      -- Not a simp lemmas as `join_cons` is more general

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