coe_treesOfNumNodesEq — Mathlib

English

The coercion of Trees(n) to sets equals the set of all x in Tree(Unit) with x.numNodes = n.

Русский

Отображение множества Trees(n) в множества равно множеству всех x в Tree(Unit) с x.numNodes = n.

LaTeX

$$$\\uparrow\\mathrm{Trees}(n) = \\{ x : \\mathrm{Tree}\\ \\mathrm{Unit} \\mid x.numNodes = n \\}$$$

Lean4

@[simp, norm_cast]
theorem coe_treesOfNumNodesEq (n : ℕ) : ↑(treesOfNumNodesEq n) = {x : Tree Unit | x.numNodes = n} :=
  Set.ext (by simp)

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