Basic

📁 Source: Mathlib/Data/Tree/Basic.lean

Statistics

Metric	Count
Definitions height, instInhabited, left, map, numLeaves, numNodes, right, traverse, unitRecOn, «term_△_», instDecidableEqTree, decEq, instReprTree, repr	14
Theorems comp_map, height_le_numNodes, id_map, left_node_right_eq_self, numLeaves_eq_numNodes_succ, numLeaves_pos, traverse_pure	7
Total	21

Tree

Definitions

Name	Category	Theorems
height 📖	CompOp	1 math math: height_le_numNodes
instInhabited 📖	CompOp	—
left 📖	CompOp	1 math math: left_node_right_eq_self
map 📖	CompOp	3 math math: comp_map, traverse_eq_map_id, id_map
numLeaves 📖	CompOp	2 math math: numLeaves_eq_numNodes_succ, numLeaves_pos
numNodes 📖	CompOp	7 math math: height_le_numNodes, numLeaves_eq_numNodes_succ, mem_treesOfNumNodesEq_numNodes, coe_treesOfNumNodesEq, mem_treesOfNumNodesEq, DyckWord.semilength_eq_numNodes_equivTree, DyckWord.numNodes_toTree
right 📖	CompOp	1 math math: left_node_right_eq_self
traverse 📖	CompOp	4 math math: traverse_pure, traverse_eq_map_id, naturality, comp_traverse
unitRecOn 📖	CompOp	—
«term_△_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_map 📖	mathematical	—	map	—	map.eq_1 map.eq_2
height_le_numNodes 📖	mathematical	—	height numNodes	—	—
id_map 📖	mathematical	—	map	—	map.eq_1 map.eq_2
left_node_right_eq_self 📖	mathematical	—	node left right	—	—
numLeaves_eq_numNodes_succ 📖	mathematical	—	numLeaves numNodes	—	—
numLeaves_pos 📖	mathematical	—	numLeaves	—	numLeaves_eq_numNodes_succ
traverse_pure 📖	mathematical	—	traverse Tree	—	traverse.eq_1 traverse.eq_2

(root)

Definitions

Name	Category	Theorems
instDecidableEqTree 📖	CompOp	1 math math: Tree.treesOfNumNodesEq_succ
instReprTree 📖	CompOp	—

instDecidableEqTree

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

instReprTree

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

---

← Back to Index