Litters

In this file, we define litters, which are the parts of an indexed partition of the base type of our model. Each litter is indexed by an element of μ, as well as some parameters β and γ used for defining the fuzz map later.

Main declarations

• ConNF.Litter: The type of litters.

structure ConNF.Litter [ConNF.Params] : Type u

The type indexing the partition of ConNF.Atom. Each atom belongs to a unique litter. The field ν : μ is an index that enforces that there are μ litters. The fields β and γ are used in the definition of the fuzz map, which is an injection into the type of litters.

• ν : ConNF.μ
• β : ConNF.TypeIndex
• γ : ConNF.Λ
• β_ne_γ : self.β ≠ ↑self.γ

theorem ConNF.instNonemptyLitter [ConNF.Params] : Nonempty ConNF.Litter

def ConNF.litterEquiv [ConNF.Params] : ConNF.Litter ≃ { a : ConNF.μ × ConNF.TypeIndex × ConNF.Λ // a.2.1 ≠ ↑a.2.2 }

Strips away the name of the type of litters, converting it into a combination of types well-known to mathlib.

Equations

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

@[simp]

theorem ConNF.card_litter [ConNF.Params] : Cardinal.mk ConNF.Litter = Cardinal.mk ConNF.μ

There are precisely μ litters.

class ConNF.SuperL (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᴸ notation. Used for converting to litters, or extracting the "litter part" of an object.

• superL : X → Y

class ConNF.SuperA (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᴬ notation. Used for converting to atoms, or extracting the "atom part" of an object.

• superA : X → Y

class ConNF.SuperN (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᴺ notation. Used for converting to near-litters, or extracting the "near-litter part" of an object.

• superN : X → Y

class ConNF.SuperU (X : Type u_1) (Y : outParam (Type u_2)) : Type (max u_1 u_2)

Typeclass for the ᵁ notation. Used for forgetful operations.

• superU : X → Y

def ConNF.«term_ᴸ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᴸ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᴸ» 1024 1024 (Lean.ParserDescr.symbol "ᴸ")

def ConNF.«term_ᴬ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᴬ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᴬ» 1024 1024 (Lean.ParserDescr.symbol "ᴬ")

def ConNF.«term_ᴺ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᴺ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᴺ» 1024 1024 (Lean.ParserDescr.symbol "ᴺ")

def ConNF.«term_ᵁ» : Lean.TrailingParserDescr

Equations

• ConNF.«term_ᵁ» = Lean.ParserDescr.trailingNode `ConNF.«term_ᵁ» 1024 1024 (Lean.ParserDescr.symbol "ᵁ")