Trees

In this file, we define the notion of a tree on a type.

Main declarations

• ConNF.Tree: The type family of trees parametrised by a given type.

def ConNF.Tree [Params] (X : Type u_1) (α : TypeIndex) : Type (max u_1 u)

An α-tree of X associates an object of type X to each path α ↝ ⊥.

Equations

• ConNF.Tree X α = (α ↝ ⊥ → X)

instance ConNF.Tree.instDerivative [Params] {X : Type u_1} {α β : TypeIndex} : Derivative (Tree X α) (Tree X β) α β

Equations

• ConNF.Tree.instDerivative = ConNF.Derivative.mk (fun (T : ConNF.Tree X α) (A : α ↝ β) (B : β ↝ ⊥) => T (A ⇘ B)) ⋯

@[simp]

theorem ConNF.Tree.deriv_apply [Params] {X : Type u_1} {α β : TypeIndex} (T : Tree X α) (A : α ↝ β) (B : β ↝ ⊥) : (T ⇘ A) B = T (A ⇘ B)

@[simp]

theorem ConNF.Tree.deriv_nil [Params] {X : Type u_1} {α : TypeIndex} (T : Tree X α) : T ⇘ Path.nil = T

theorem ConNF.Tree.deriv_deriv [Params] {X : Type u_1} {α β γ : TypeIndex} (T : Tree X α) (A : α ↝ β) (B : β ↝ γ) : T ⇘ A ⇘ B = T ⇘ (A ⇘ B)

theorem ConNF.Tree.deriv_sderiv [Params] {X : Type u_1} {α β γ : TypeIndex} (T : Tree X α) (A : α ↝ β) (h : γ < β) : T ⇘ A ↘ h = T ⇘ (A ↘ h)

@[simp]

theorem ConNF.Tree.sderiv_apply [Params] {X : Type u_1} {α β : TypeIndex} (T : Tree X α) (h : β < α) (B : β ↝ ⊥) : (T ↘ h) B = T (B ↗ h)

instance ConNF.Tree.instBotDerivative [Params] {X : Type u_1} {α : TypeIndex} : BotDerivative (Tree X α) X α

Equations

• ConNF.Tree.instBotDerivative = ConNF.BotDerivative.mk (fun (T : ConNF.Tree X α) (A : α ↝ ⊥) => T A) ⋯

@[simp]

theorem ConNF.Tree.botDeriv_eq [Params] {X : Type u_1} {α : TypeIndex} (T : Tree X α) (A : α ↝ ⊥) : T ⇘. A = T A

theorem ConNF.Tree.botSderiv_eq [Params] {X : Type u_1} {α : TypeIndex} (T : Tree X α) : T ↘. = T (Path.nil ↘.)

instance ConNF.Tree.group [Params] {X : Type u_1} {α : TypeIndex} [Group X] : Group (Tree X α)

The group structure on the type of α-trees of X is given by "branchwise" multiplication, given by Pi.group.

Equations

• ConNF.Tree.group = Pi.group

@[simp]

theorem ConNF.Tree.one_apply [Params] {X : Type u_1} {α : TypeIndex} [Group X] (A : α ↝ ⊥) : 1 A = 1

@[simp]

theorem ConNF.Tree.one_deriv [Params] {X : Type u_1} {α β : TypeIndex} [Group X] (A : α ↝ β) : 1 ⇘ A = 1

@[simp]

theorem ConNF.Tree.one_sderiv [Params] {X : Type u_1} {α β : TypeIndex} [Group X] (h : β < α) : 1 ↘ h = 1

@[simp]

theorem ConNF.Tree.one_sderivBot [Params] {X : Type u_1} {α : TypeIndex} [Group X] : 1 ↘. = 1

@[simp]

theorem ConNF.Tree.mul_apply [Params] {X : Type u_1} {α : TypeIndex} [Group X] (T₁ T₂ : Tree X α) (A : α ↝ ⊥) : (T₁ * T₂) A = T₁ A * T₂ A

@[simp]

theorem ConNF.Tree.mul_deriv [Params] {X : Type u_1} {α β : TypeIndex} [Group X] (T₁ T₂ : Tree X α) (A : α ↝ β) : (T₁ * T₂) ⇘ A = T₁ ⇘ A * T₂ ⇘ A

@[simp]

theorem ConNF.Tree.mul_sderiv [Params] {X : Type u_1} {α β : TypeIndex} [Group X] (T₁ T₂ : Tree X α) (h : β < α) : (T₁ * T₂) ↘ h = T₁ ↘ h * T₂ ↘ h

@[simp]

theorem ConNF.Tree.mul_sderivBot [Params] {X : Type u_1} {α : TypeIndex} [Group X] (T₁ T₂ : Tree X α) : (T₁ * T₂) ↘. = T₁ ↘. * T₂ ↘.

@[simp]

theorem ConNF.Tree.inv_apply [Params] {X : Type u_1} {α : TypeIndex} [Group X] (T : Tree X α) (A : α ↝ ⊥) : T⁻¹ A = (T A)⁻¹

@[simp]

theorem ConNF.Tree.inv_deriv [Params] {X : Type u_1} {α β : TypeIndex} [Group X] (T : Tree X α) (A : α ↝ β) : T⁻¹ ⇘ A = (T ⇘ A)⁻¹

@[simp]

theorem ConNF.Tree.inv_sderiv [Params] {X : Type u_1} {α β : TypeIndex} [Group X] (T : Tree X α) (h : β < α) : T⁻¹ ↘ h = (T ↘ h)⁻¹

@[simp]

theorem ConNF.Tree.inv_sderivBot [Params] {X : Type u_1} {α : TypeIndex} [Group X] (T : Tree X α) : T⁻¹ ↘. = (T ↘.)⁻¹

@[simp]

theorem ConNF.Tree.npow_apply [Params] {X : Type u_1} {α : TypeIndex} [Group X] (T : Tree X α) (A : α ↝ ⊥) (n : ℕ) : (T ^ n) A = T A ^ n

@[simp]

theorem ConNF.Tree.zpow_apply [Params] {X : Type u_1} {α : TypeIndex} [Group X] (T : Tree X α) (A : α ↝ ⊥) (n : ℤ) : (T ^ n) A = T A ^ n

instance ConNF.Tree.partialOrder [Params] {X : Type u_1} {α : TypeIndex} [PartialOrder X] : PartialOrder (Tree X α)

The partial order on the type of α-trees of X is given by "branchwise" comparison.

Equations

• ConNF.Tree.partialOrder = Pi.partialOrder

theorem ConNF.Tree.le_iff [Params] {X : Type u_1} {α : TypeIndex} [PartialOrder X] (T₁ T₂ : Tree X α) : T₁ ≤ T₂ ↔ ∀ (A : α ↝ ⊥), T₁ A ≤ T₂ A

Cardinality bounds on trees

theorem ConNF.card_tree_le [Params] {X : Type u} {α : TypeIndex} (h : Cardinal.mk X ≤ Cardinal.mk μ) : Cardinal.mk (Tree X α) ≤ Cardinal.mk μ

theorem ConNF.card_tree_lt [Params] {X : Type u} {α : TypeIndex} (h : Cardinal.mk X < Cardinal.mk μ) : Cardinal.mk (Tree X α) < Cardinal.mk μ

theorem ConNF.card_tree_eq [Params] {X : Type u} {α : TypeIndex} (h : Cardinal.mk X = Cardinal.mk μ) : Cardinal.mk (Tree X α) = Cardinal.mk μ