Supports

In this file, we define addresses and supports.

Main declarations

• ConNF.Address: The type of addresses.
• ConNF.Support: The type of small supports made of addresses.

theorem ConNF.Address.ext_iff : ∀ {inst : ConNF.Params} {α : ConNF.TypeIndex} (x y : ConNF.Address α), x = y ↔ x.path = y.path ∧ x.value = y.value

theorem ConNF.Address.ext : ∀ {inst : ConNF.Params} {α : ConNF.TypeIndex} (x y : ConNF.Address α), x.path = y.path → x.value = y.value → x = y

structure ConNF.Address [ConNF.Params] (α : ConNF.TypeIndex) : Type u

A address is an extended type index together with an atom or a near-litter. This represents an object in the base type (the atom or near-litter) together with the path detailing how we descend from type α to type ⊥ by looking at elements of elements and so on in the model.

• path : ConNF.ExtendedIndex α
• value : ConNF.Atom ⊕ ConNF.NearLitter

def ConNF.Address_equiv [ConNF.Params] {α : ConNF.TypeIndex} : ConNF.Address α ≃ ConNF.ExtendedIndex α × (ConNF.Atom ⊕ ConNF.NearLitter)

Equations

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

@[simp]

theorem ConNF.mk_address [ConNF.Params] (α : ConNF.TypeIndex) : Cardinal.mk (ConNF.Address α) = Cardinal.mk ConNF.μ

There are μ addresses.

instance ConNF.StructPerm.instMulActionAddress [ConNF.Params] {α : ConNF.TypeIndex} : MulAction (ConNF.StructPerm α) (ConNF.Address α)

Structural permutations act on addresses by following the derivative given in the condition.

Equations

• ConNF.StructPerm.instMulActionAddress = MulAction.mk ⋯ ⋯

We have a form of the next three lemmas for StructPerm, BasePerm, Allowable, and NewAllowable.

theorem ConNF.StructPerm.smul_address [ConNF.Params] {α : ConNF.TypeIndex} {π : ConNF.StructPerm α} {c : ConNF.Address α} : π • c = { path := c.path, value := π c.path • c.value }

@[simp]

theorem ConNF.StructPerm.smul_address_eq_iff [ConNF.Params] {α : ConNF.TypeIndex} {π : ConNF.StructPerm α} {c : ConNF.Address α} : π • c = c ↔ π c.path • c.value = c.value

@[simp]

theorem ConNF.StructPerm.smul_address_eq_smul_iff [ConNF.Params] {α : ConNF.TypeIndex} {π : ConNF.StructPerm α} {π' : ConNF.StructPerm α} {c : ConNF.Address α} : π • c = π' • c ↔ π c.path • c.value = π' c.path • c.value

instance ConNF.BasePerm.instMulActionAddressBotTypeIndex [ConNF.Params] : MulAction ConNF.BasePerm (ConNF.Address ⊥)

Equations

• ConNF.BasePerm.instMulActionAddressBotTypeIndex = MulAction.mk ⋯ ⋯

theorem ConNF.BasePerm.smul_address [ConNF.Params] {π : ConNF.BasePerm} {c : ConNF.Address ⊥} : π • c = { path := c.path, value := π • c.value }

@[simp]

theorem ConNF.BasePerm.smul_address_eq_iff [ConNF.Params] {π : ConNF.BasePerm} {c : ConNF.Address ⊥} : π • c = c ↔ π • c.value = c.value

@[simp]

theorem ConNF.BasePerm.smul_address_eq_smul_iff [ConNF.Params] {π : ConNF.BasePerm} {π' : ConNF.BasePerm} {c : ConNF.Address ⊥} : π • c = π' • c ↔ π • c.value = π' • c.value

@[reducible, inline]

abbrev ConNF.Support [ConNF.Params] (α : ConNF.TypeIndex) : Type u

A support is a function from an initial segment of κ to the type of addresses.

Equations

• ConNF.Support α = ConNF.Enumeration (ConNF.Address α)

@[simp]

theorem ConNF.mk_support [ConNF.Params] {α : ConNF.TypeIndex} : Cardinal.mk (ConNF.Support α) = Cardinal.mk ConNF.μ

There are exactly μ supports.

theorem ConNF.support_f_congr [ConNF.Params] {α : ConNF.TypeIndex} {S : ConNF.Support α} {T : ConNF.Support α} (h : S = T) (i : ConNF.κ) (hS : i < S.max) : S.f i hS = T.f i ⋯

A useful lemma that avoids the hypothesis i < T.max.