Construction of position functions

Assuming that there are only μ t-sets at level α, we can construct a position function for them.

Main declarations

• CoNNF.Construction.pos: A position function for type α t-sets.

def ConNF.Construction.posBound [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t : ConNF.NewTSet) (S : ConNF.Support ↑ConNF.α) : Set ConNF.μ

The position of t must be greater than elements of this small set. Since it is small, it cannot be cofinal in μ.

Equations

• One or more equations did not get rendered due to their size.

def ConNF.Construction.posBound' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t : ConNF.NewTSet) (S : ConNF.Support ↑ConNF.α) : Set ConNF.μ

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.Construction.posBound_eq_posBound' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t : ConNF.NewTSet) (S : ConNF.Support ↑ConNF.α) : ConNF.Construction.posBound t S = ConNF.Construction.posBound' t S

theorem ConNF.Construction.small_posBound [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t : ConNF.NewTSet) (S : ConNF.Support ↑ConNF.α) : ConNF.Small (ConNF.Construction.posBound t S)

def ConNF.Construction.posDeny [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t : ConNF.NewTSet × ConNF.Support ↑ConNF.α) : Set ConNF.μ

The position of t must be greater than elements of this set, which is not cofinal in μ.

Equations

• ConNF.Construction.posDeny t = {ν : ConNF.μ | ∃ ν' ∈ ConNF.Construction.posBound t.1 t.2, ν ≤ ν'}

theorem ConNF.Construction.mk_posDeny [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (t : ConNF.NewTSet × ConNF.Support ↑ConNF.α) : Cardinal.mk ↑(ConNF.Construction.posDeny t) < Cardinal.mk ConNF.μ

theorem ConNF.Construction.exists_wellOrder [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) : ∃ (r : ConNF.NewTSet × ConNF.Support ↑ConNF.α → ConNF.NewTSet × ConNF.Support ↑ConNF.α → Prop) (x : IsWellOrder (ConNF.NewTSet × ConNF.Support ↑ConNF.α) r), Ordinal.type r = (Cardinal.mk ConNF.μ).ord

def ConNF.Construction.wellOrder [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) : ConNF.NewTSet × ConNF.Support ↑ConNF.α → ConNF.NewTSet × ConNF.Support ↑ConNF.α → Prop

Equations

• ConNF.Construction.wellOrder h = ⋯.choose

instance ConNF.Construction.wellOrder_isWellOrder [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) : IsWellOrder (ConNF.NewTSet × ConNF.Support ↑ConNF.α) (ConNF.Construction.wellOrder h)

Equations

• ⋯ = ⋯

theorem ConNF.Construction.wellOrder_type [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) : Ordinal.type (ConNF.Construction.wellOrder h) = (Cardinal.mk ConNF.μ).ord

theorem ConNF.Construction.mk_posDeny' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) (t : ConNF.NewTSet × ConNF.Support ↑ConNF.α) : Cardinal.mk { s : ConNF.NewTSet × ConNF.Support ↑ConNF.α // ConNF.Construction.wellOrder h s t } + Cardinal.mk ↑(ConNF.Construction.posDeny t) < Cardinal.mk ConNF.μ

noncomputable def ConNF.Construction.pos [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) : ConNF.NewTSet × ConNF.Support ↑ConNF.α → ConNF.μ

A position function for type α t-sets.

Equations

• ConNF.Construction.pos h = ConNF.chooseWf ConNF.Construction.posDeny ⋯

theorem ConNF.Construction.pos_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) : Function.Injective (ConNF.Construction.pos h)

theorem ConNF.Construction.pos_not_mem_deny [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.ModelDataLt] [ConNF.PositionedTanglesLt] [ConNF.TypedObjectsLt] [ConNF.PositionedObjectsLt] (h : Cardinal.mk ConNF.NewTSet = Cardinal.mk ConNF.μ) (t : ConNF.NewTSet × ConNF.Support ↑ConNF.α) : ConNF.Construction.pos h t ∉ ConNF.Construction.posDeny t