Position functions

In this file, we define what it means for a type to have a position function.

Main declarations

• ConNF.Position: The typeclass that stores a position function for a type.

class ConNF.Position [ConNF.Params] (X : Type u_1) : Type (max u u_1)

• pos : X ↪ ConNF.μ

theorem ConNF.card_le_of_position [ConNF.Params] {X : Type u} [ConNF.Position X] : Cardinal.mk X ≤ Cardinal.mk ConNF.μ

def ConNF.pos_induction [ConNF.Params] {X : Type u_1} [ConNF.Position X] {C : X → Prop} (x : X) (h : ∀ (x : X), (∀ (y : X), ConNF.pos y < ConNF.pos x → C y) → C x) : C x

Equations

• ⋯ = ⋯