def ConNF.SpecCondition' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) : Type u

Equations

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

def ConNF.SpecCondition.toPrime [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : ConNF.SpecCondition β → ConNF.SpecCondition' β

Equations

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

theorem ConNF.SpecCondition.toPrime_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} : Function.Injective ConNF.SpecCondition.toPrime

def ConNF.InflexibleCoePath' [ConNF.Params] (β : ConNF.Λ) : Type u

Equations

• ConNF.InflexibleCoePath' β = (ConNF.Λ × ConNF.Λ × ConNF.Λ × ConNF.ExtendedIndex ↑β)

def ConNF.InflexibleCoePath'.toPrime [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (h : ConNF.InflexibleCoePath A) : ConNF.InflexibleCoePath' β

Equations

• ConNF.InflexibleCoePath'.toPrime h = (h.γ, h.δ, h.ε, h.B.cons ⋯)

theorem ConNF.InflexibleCoePath'.toPrime_injective [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} : Function.Injective ConNF.InflexibleCoePath'.toPrime

theorem ConNF.mk_inflexibleCoePath [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) : Cardinal.mk (ConNF.InflexibleCoePath A) ≤ Cardinal.mk ConNF.Λ

def ConNF.InflexibleBotPath' [ConNF.Params] (β : ConNF.Λ) : Type u

Equations

• ConNF.InflexibleBotPath' β = (ConNF.Λ × ConNF.Λ × ConNF.ExtendedIndex ↑β)

def ConNF.InflexibleBotPath'.toPrime [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} (h : ConNF.InflexibleBotPath A) : ConNF.InflexibleBotPath' β

Equations

• ConNF.InflexibleBotPath'.toPrime h = (h.γ, h.ε, h.B.cons ⋯)

theorem ConNF.InflexibleBotPath'.toPrime_injective [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} {A : ConNF.ExtendedIndex ↑β} : Function.Injective ConNF.InflexibleBotPath'.toPrime

theorem ConNF.mk_inflexibleBotPath [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} (A : ConNF.ExtendedIndex ↑β) : Cardinal.mk (ConNF.InflexibleBotPath A) ≤ Cardinal.mk ConNF.Λ

theorem ConNF.mk_specCondition [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (h : ∀ (δ : ConNF.Λ) [inst : ConNF.LeLevel ↑δ], δ < β → Cardinal.mk (ConNF.CodingFunction δ) < Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.SpecCondition β) < Cardinal.mk ConNF.μ

theorem ConNF.mk_spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (h : ∀ (δ : ConNF.Λ) [inst : ConNF.LeLevel ↑δ], δ < β → Cardinal.mk (ConNF.CodingFunction δ) < Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.Spec β) < Cardinal.mk ConNF.μ