treesOfNumNodesEq_succ — Mathlib

English

For every n, Trees(n+1) equals the union over all pairs (i,j) in Antidiagonal(n) of pairwiseNode(Trees(i), Trees(j)).

Русский

Для каждого n множество Trees(n+1) равно объединению по всем парам (i,j) из Antidiagonal(n) парного узеления: pairwiseNode(Trees(i), Trees(j)).

LaTeX

$$$\\mathrm{Trees}(n+1) = \\bigcup_{(i,j)\\in \\mathrm{Antidiagonal}(n)} \\mathrm{pairwiseNode}(\\mathrm{Trees}(i), \\mathrm{Trees}(j)).$$$

Lean4

theorem treesOfNumNodesEq_succ (n : ℕ) :
    treesOfNumNodesEq (n + 1) =
      (antidiagonal n).biUnion fun ij => pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2) :=
  by
  rw [treesOfNumNodesEq]
  ext
  simp

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