join_cons_cons — Mathlib

English

Joining a stream whose head is a pair of a and a stream starting with b and s yields the head a and the join of the rest.

Русский

Объединение потока с головой (a, конс) или подобную форму даёт головной элемент a и последующий join.

LaTeX

$$$\forall a b s S,\; join (cons (a, cons b s) S) = cons a (join (cons (b, s) S))$$$

Lean4

theorem join_cons_cons (a b : α) (s S) : join (cons (a, cons b s) S) = cons a (join (cons (b, s) S)) :=
  destruct_eq_cons <| by simp [join]

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