Equivalences

This section contains theorems about equivalences between different tree indexing types and data structures.

def BinaryTree.LeafData.ofFun {α : Type} (s : Skeleton) (f : SkeletonLeafIndex s → α) : LeafData α s

Build LeafData from a function on leaf indices.

@[simp]

theorem BinaryTree.LeafData.ofFun_get {α : Type} {s : Skeleton} (tree : LeafData α s) : (ofFun s fun (idx : SkeletonLeafIndex s) => tree.get idx) = tree

@[simp]

theorem BinaryTree.LeafData.get_ofFun {α : Type} {s : Skeleton} (f : SkeletonLeafIndex s → α) : (ofFun s f).get = f

def BinaryTree.InternalData.ofFun {α : Type} (s : Skeleton) (f : SkeletonInternalIndex s → α) : InternalData α s

Build InternalData from a function on internal indices.

@[simp]

theorem BinaryTree.InternalData.ofFun_get {α : Type} {s : Skeleton} (tree : InternalData α s) : (ofFun s fun (idx : SkeletonInternalIndex s) => tree.get idx) = tree

@[simp]

theorem BinaryTree.InternalData.get_ofFun {α : Type} {s : Skeleton} (f : SkeletonInternalIndex s → α) : (ofFun s f).get = f

def BinaryTree.FullData.ofFun {α : Type} (s : Skeleton) (f : SkeletonNodeIndex s → α) : FullData α s

Build FullData from a function on all node indices.

@[simp]

theorem BinaryTree.FullData.ofFun_get {α : Type} {s : Skeleton} (tree : FullData α s) : (ofFun s fun (idx : SkeletonNodeIndex s) => tree.get idx) = tree

@[simp]

theorem BinaryTree.FullData.get_ofFun {α : Type} {s : Skeleton} (f : SkeletonNodeIndex s → α) : (ofFun s f).get = f

def BinaryTree.LeafData.EquivIndexFun {α : Type} (s : Skeleton) : LeafData α s ≃ (SkeletonLeafIndex s → α)

LeafDatas are equivalent to functions from SkeletonLeafIndex to values

def BinaryTree.InternalData.EquivIndexFun {α : Type} (s : Skeleton) : InternalData α s ≃ (SkeletonInternalIndex s → α)

InternalDatas are equivalent to functions from SkeletonInternalIndex to values

def BinaryTree.FullData.EquivIndexFun {α : Type} (s : Skeleton) : FullData α s ≃ (SkeletonNodeIndex s → α)

FullDatas are equivalent to functions from SkeletonNodeIndex to values

instance BinaryTree.instCoeFunLeafDataForallSkeletonLeafIndex {α : Type} {s : Skeleton} : CoeFun (LeafData α s) fun (x : LeafData α s) => SkeletonLeafIndex s → α

A LeafData can be interpreted as a function from SkeletonLeafIndex to values

instance BinaryTree.instCoeFunInternalDataForallSkeletonInternalIndex {α : Type} {s : Skeleton} : CoeFun (InternalData α s) fun (x : InternalData α s) => SkeletonInternalIndex s → α

An InternalData can be interpreted as a function from SkeletonInternalIndex to values

instance BinaryTree.instCoeFunFullDataForallSkeletonNodeIndex {α : Type} {s : Skeleton} : CoeFun (FullData α s) fun (x : FullData α s) => SkeletonNodeIndex s → α

A FullData can be interpreted as a function from SkeletonNodeIndex to values

def BinaryTree.SkeletonNodeIndex.toSum {s : Skeleton} : SkeletonNodeIndex s → SkeletonInternalIndex s ⊕ SkeletonLeafIndex s

A function taking a SkeletonNodeIndex s to either a SkeletonInternalIndex s or a SkeletonLeafIndex s

def BinaryTree.SkeletonNodeIndex.SumEquiv (s : Skeleton) : SkeletonInternalIndex s ⊕ SkeletonLeafIndex s ≃ SkeletonNodeIndex s

def BinaryTree.Equiv.precomp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) : (β → γ) ≃ (α → γ)

def BinaryTree.SumFunEquivProd (α β γ : Type) : (α ⊕ β → γ) ≃ (α → γ) × (β → γ)

def BinaryTree.FullData.Equiv {α : Type} (s : Skeleton) : FullData α s ≃ InternalData α s × LeafData α s

Equivalence between FullData and the product of InternalData and LeafData