Unique maps for FourTree

We define the uniqueMap4 and uniqueMap3 functions for FourTree. For a given f : α4 → α4 or f : α3 → α3, these functions the elements of a FourTree, and leave only new elements which are not already present in the tree (if the tree has no duplicates).

uniqueMap4

def PhysLean.FourTree.Leaf.uniqueMap4 {α4 : Type} (f : α4 → α4) : Leaf α4 → Leaf α4

Given a map f : α4 → α4 the map from Leaf α4 → Leaf α4 mapping the underlying elements.

Equations

• PhysLean.FourTree.Leaf.uniqueMap4 f (PhysLean.FourTree.Leaf.leaf x_1) = PhysLean.FourTree.Leaf.leaf (f x_1)

def PhysLean.FourTree.Twig.uniqueMap4 {α3 α4 : Type} [DecidableEq α4] (f : α4 → α4) (T : Twig α3 α4) : Twig α3 α4

Given a map f : α4 → α4 the map from Twig α3 α4 → Twig α3 α4 mapping the underlying leafs and deleting any that appear in the original Twig.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.FourTree.Branch.uniqueMap4 {α2 α3 α4 : Type} [DecidableEq α4] (f : α4 → α4) (T : Branch α2 α3 α4) : Branch α2 α3 α4

Given a map f : α4 → α4 the map from Branch α2 α3 α4 → Branch α2 α3 α4 mapping the underlying leafs and deleting any that appear in the original Twig.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.FourTree.Trunk.uniqueMap4 {α1 α2 α3 α4 : Type} [DecidableEq α4] (f : α4 → α4) (T : Trunk α1 α2 α3 α4) : Trunk α1 α2 α3 α4

Given a map f : α4 → α4 the map from Trunk α1 α2 α3 α4 → Trunk α1 α2 α3 α4 mapping the underlying leafs and deleting any that appear in the original Twig.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.FourTree.uniqueMap4 {α1 α2 α3 α4 : Type} [DecidableEq α4] (f : α4 → α4) (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4

Given a map f : α4 → α4 the map from FourTree α1 α2 α3 α4 → FourTree α1 α2 α3 α4 mapping the underlying leafs and deleting any that appear in the original twig of that leaf.

Equations

• One or more equations did not get rendered due to their size.

theorem PhysLean.FourTree.map_mem_uniqueMap4 {α1 α2 α3 α4 : Type} [DecidableEq α4] {T : FourTree α1 α2 α3 α4} (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α4 → α4) : (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ uniqueMap4 f T ∨ (x.1, x.2.1, x.2.2.1, f x.2.2.2) ∈ T

theorem PhysLean.FourTree.exists_of_mem_uniqueMap4 {α1 α2 α3 α4 : Type} [DecidableEq α4] (f : α4 → α4) {T : FourTree α1 α2 α3 α4} (C : α1 × α2 × α3 × α4) (h : C ∈ uniqueMap4 f T) : ∃ (qHd : α1) (qHu : α2) (Q5 : α3) (Q10 : α4), C = (qHd, qHu, Q5, f Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T

uniqueMap3

def PhysLean.FourTree.Twig.uniqueMap3 {α3 α4 : Type} (f : α3 → α3) (T : Twig α3 α4) : Twig α3 α4

Given a map f : α3 → α3 the map from Twig α3 α4 → Twig α3 α4 mapping the underlying first value of the twig.

Equations

• PhysLean.FourTree.Twig.uniqueMap3 f (PhysLean.FourTree.Twig.twig xs leafs) = PhysLean.FourTree.Twig.twig (f xs) leafs

def PhysLean.FourTree.Branch.uniqueMap3 {α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (f : α3 → α3) (T : Branch α2 α3 α4) : Branch α2 α3 α4

Given a map f : α3 → α3 the map from Branch α2 α3 α4 → Branch α2 α3 α4 mapping the underlying first value of the twig, and deleting any new leafs that appeared in the old branch.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.FourTree.Trunk.uniqueMap3 {α1 α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (f : α3 → α3) (T : Trunk α1 α2 α3 α4) : Trunk α1 α2 α3 α4

Given a map f : α3 → α3 the map from Trunk α1 α2 α3 α4 → Trunk α1 α2 α3 α4 mapping the underlying first value of the twig, and deleting any new leafs that appeared in the old branch.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.FourTree.uniqueMap3 {α1 α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (f : α3 → α3) (T : FourTree α1 α2 α3 α4) : FourTree α1 α2 α3 α4

Given a map f : α3 → α3 the map from FourTree α1 α2 α3 α4 → FourTree α1 α2 α3 α4 mapping the underlying first value of the twig, and deleting any new leafs that appeared in the old branch.

Equations

• One or more equations did not get rendered due to their size.

theorem PhysLean.FourTree.map_mem_uniqueMap3 {α1 α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] {T : FourTree α1 α2 α3 α4} (x : α1 × α2 × α3 × α4) (hx : x ∈ T) (f : α3 → α3) : (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ uniqueMap3 f T ∨ (x.1, x.2.1, f x.2.2.1, x.2.2.2) ∈ T

theorem PhysLean.FourTree.exists_of_mem_uniqueMap3 {α1 α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (f : α3 → α3) {T : FourTree α1 α2 α3 α4} (C : α1 × α2 × α3 × α4) (h : C ∈ uniqueMap3 f T) : ∃ (qHd : α1) (qHu : α2) (Q5 : α3) (Q10 : α4), C = (qHd, qHu, f Q5, Q10) ∧ (qHd, qHu, Q5, Q10) ∈ T