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.

source

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

Type (max u_1 u)

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

Equations

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

Instances For

source

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

ConNF.Derivative (ConNF.Tree X α) (ConNF.Tree X β) α β

Equations

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

source

@[simp]

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

(T ⇘ A) B = T (A ⇘ B)

source

@[simp]

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

T ⇘ ConNF.Path.nil = T

source

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

T ⇘ A ⇘ B = T ⇘ (A ⇘ B)

source

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

T ⇘ A ↘ h = T ⇘ (A ↘ h)

source

@[simp]

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

(T ↘ h) B = T (B ↗ h)

source

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

ConNF.BotDerivative (ConNF.Tree X α) X α

Equations

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

source

@[simp]

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

T ⇘. A = T A

source

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

T ↘. = T (ConNF.Path.nil ↘.)

source

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

Group (ConNF.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

source

@[simp]

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

1 A = 1

source

@[simp]

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

1 ⇘ A = 1

source

@[simp]

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

1 ↘ h = 1

source

@[simp]

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

1 ↘. = 1

source

@[simp]

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

(T₁ * T₂) A = T₁ A * T₂ A

source

@[simp]

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

(T₁ * T₂) ⇘ A = T₁ ⇘ A * T₂ ⇘ A

source

@[simp]

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

(T₁ * T₂) ↘ h = T₁ ↘ h * T₂ ↘ h

source

@[simp]

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

(T₁ * T₂) ↘. = T₁ ↘. * T₂ ↘.

source

@[simp]

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

T⁻¹ A = (T A)⁻¹

source

@[simp]

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

T⁻¹ ⇘ A = (T ⇘ A)⁻¹

source

@[simp]

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

T⁻¹ ↘ h = (T ↘ h)⁻¹

source

@[simp]

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

T⁻¹ ↘. = (T ↘.)⁻¹

source

@[simp]

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

(T ^ n) A = T A ^ n

source

@[simp]

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

(T ^ n) A = T A ^ n

source

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

PartialOrder (ConNF.Tree X α)

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

Equations

ConNF.Tree.partialOrder = Pi.partialOrder

source

theorem ConNF.Tree.le_iff [ConNF.Params] {X : Type u_1} {α : ConNF.TypeIndex} [PartialOrder X] (T₁ T₂ : ConNF.Tree X α) :

T₁ ≤ T₂ ↔ ∀ (A : α ↝ ⊥), T₁ A ≤ T₂ A

Cardinality bounds on trees #

source

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

Cardinal.mk (ConNF.Tree X α) ≤ Cardinal.mk ConNF.μ

source

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

Cardinal.mk (ConNF.Tree X α) < Cardinal.mk ConNF.μ

source

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

Cardinal.mk (ConNF.Tree X α) = Cardinal.mk ConNF.μ

Documentation

ConNF.Levels.Tree

Trees #

Main declarations #

Cardinality bounds on trees #