mem_treesOfNumNodesEq — Mathlib

English

For a tree x and a nonnegative integer n, x belongs to Trees(n) if and only if x.numNodes = n.

Русский

Для дерева x и числа n: x ∈ Trees(n) тогда и только тогда, когда x.numNodes = n.

LaTeX

$$$x \\in \\mathrm{Trees}(n) \\iff x.{\\tt numNodes} = n$$$

Lean4

@[simp]
theorem mem_treesOfNumNodesEq {x : Tree Unit} {n : ℕ} : x ∈ treesOfNumNodesEq n ↔ x.numNodes = n := by
  induction x using Tree.unitRecOn generalizing n <;> cases n <;> simp [treesOfNumNodesEq_succ, *]

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