Depth

📁 Source: Batteries/Data/RBMap/Depth.lean

Statistics

Metric	Count
Definitions depth, depthLB, depthUB	3
Theorems depth_bound, depth_le, le_size, depth_bound, depthLB_le, depthUB_le, depthUB_le_two_depthLB, size_lt_depth	8
Total	11

Batteries.RBNode

Definitions

Name	Category	Theorems
depth 📖	CompOp	4 math math: WF.depth_bound, size_lt_depth, Balanced.depth_le, Balanced.depth_bound
depthLB 📖	CompOp	3 math math: depthLB_le, Balanced.le_size, depthUB_le_two_depthLB
depthUB 📖	CompOp	3 math math: depthUB_le, depthUB_le_two_depthLB, Balanced.depth_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
depthLB_le 📖	mathematical	—	depthLB	—	—
depthUB_le 📖	mathematical	—	depthUB	—	—
depthUB_le_two_depthLB 📖	mathematical	—	depthUB depthLB	—	—
size_lt_depth 📖	mathematical	—	size depth	—	size.eq_2 depth.eq_2

Batteries.RBNode.Balanced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
depth_bound 📖	mathematical	Batteries.RBNode.Balanced	Batteries.RBNode.depth Batteries.RBNode.size	—	depth_le Batteries.RBNode.depthUB_le_two_depthLB le_size
depth_le 📖	mathematical	Batteries.RBNode.Balanced	Batteries.RBNode.depth Batteries.RBNode.depthUB	—	Batteries.RBNode.depthUB_le
le_size 📖	mathematical	Batteries.RBNode.Balanced	Batteries.RBNode.depthLB Batteries.RBNode.size	—	Batteries.RBNode.size.eq_2 Batteries.RBNode.depthLB.eq_1 Batteries.RBNode.depthLB.eq_2 Batteries.RBNode.depthLB_le

Batteries.RBNode.WF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
depth_bound 📖	mathematical	Batteries.RBNode.WF	Batteries.RBNode.depth Batteries.RBNode.size	—	out Batteries.RBNode.Balanced.depth_bound

---

← Back to Index