Documentation

ConNF.Base.TypeIndex

Type indices #

In this file, we declare the notion of a type index, and prove some of its basic properties.

Main declarations #

source
@[reducible]
def ConNF.TypeIndex [ConNF.Params] :
Type u

Either the base type or a proper type index (an inhabitant of Λ). The base type is written ⊥.

Equations
Instances For
    source
    instance ConNF.instWellFoundedRelationTypeIndex [ConNF.Params] :
    WellFoundedRelation ConNF.TypeIndex

    Allows us to use termination_by clauses with TypeIndex.

    Equations
    • ConNF.instWellFoundedRelationTypeIndex = { rel := fun (x1 x2 : ConNF.TypeIndex) => x1 < x2, wf := ⋯ }
    source
    @[simp]
    theorem ConNF.TypeIndex.type [ConNF.Params] :
    (Ordinal.type fun (x1 x2 : ConNF.TypeIndex) => x1 < x2) = Ordinal.type fun (x1 x2 : ConNF.Λ) => x1 < x2
    source
    @[simp]
    theorem ConNF.TypeIndex.card [ConNF.Params] :
    Cardinal.mk ConNF.TypeIndex = Cardinal.mk ConNF.Λ
    source
    theorem ConNF.Λ_card_Iio_lt [ConNF.Params] (α : ConNF.Λ) :
    Cardinal.mk ↑{β : ConNF.Λ | β < α} < (Cardinal.mk ConNF.μ).ord.cof
    source
    theorem ConNF.Λ_card_Iic_lt [ConNF.Params] (α : ConNF.Λ) :
    Cardinal.mk ↑{β : ConNF.Λ | β ≤ α} < (Cardinal.mk ConNF.μ).ord.cof
    source
    theorem ConNF.TypeIndex.card_Iio_lt [ConNF.Params] (α : ConNF.TypeIndex) :
    Cardinal.mk ↑{β : ConNF.TypeIndex | β < α} < (Cardinal.mk ConNF.μ).ord.cof
    source
    theorem ConNF.TypeIndex.card_Iic_lt [ConNF.Params] (α : ConNF.TypeIndex) :
    Cardinal.mk ↑{β : ConNF.TypeIndex | β ≤ α} < (Cardinal.mk ConNF.μ).ord.cof