Position functions

In this file, we define position functions. Position functions taking values in μ are used to give orders on types such as tangles.

Main declarations

• ConNF.Position: A class that provides a function pos : α ↪ β.

class ConNF.Position (α : Type u_1) (β : outParam (Type u_2)) : Type (max u_1 u_2)

• pos : α ↪ β

theorem ConNF.pos_injective {α : Type u_1} {β : Type u_2} [ConNF.Position α β] : Function.Injective ⇑ConNF.pos

instance ConNF.instLT_conNF {α : Type u_1} {β : Type u_2} [ConNF.Position α β] [LT β] : LT α

Equations

• ConNF.instLT_conNF = { lt := InvImage (fun (x x_1 : β) => x < x_1) ⇑ConNF.pos }

theorem ConNF.pos_lt_pos {α : Type u_2} {β : Type u_1} [ConNF.Position α β] [LT β] (c : α) (d : α) : ConNF.pos c < ConNF.pos d ↔ c < d

theorem ConNF.isWellOrder_invImage {α : Type u_2} {β : Type u_1} {r : β → β → Prop} (h : IsWellOrder β r) (f : α → β) (hf : Function.Injective f) : IsWellOrder α (InvImage r f)

instance ConNF.instIsWellOrderLt_conNF {α : Type u_2} {β : Type u_1} [ConNF.Position α β] [LT β] [IsWellOrder β fun (x x_1 : β) => x < x_1] : IsWellOrder α fun (x x_1 : α) => x < x_1

Equations

• ⋯ = ⋯

instance ConNF.instIsWellOrderInvImageLtCoeEmbeddingPos {α : Type u_2} {β : Type u_1} [ConNF.Position α β] [LT β] [IsWellOrder β fun (x x_1 : β) => x < x_1] : IsWellOrder α (InvImage (fun (x x_1 : β) => x < x_1) ⇑ConNF.pos)

Equations

• ⋯ = ⋯

instance ConNF.instWellFoundedRelationOfIsWellOrderLt_conNF {α : Type u_1} {β : Type u_2} [ConNF.Position α β] [LT β] [IsWellOrder β fun (x x_1 : β) => x < x_1] : WellFoundedRelation α

Equations

• ConNF.instWellFoundedRelationOfIsWellOrderLt_conNF = IsWellOrder.toHasWellFounded