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 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.Litter.β_ne_γ [ConNF.Params] (self : ConNF.Litter) : self.β ≠ ↑self.γ

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

Equations

• ⋯ = ⋯

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.mk_litter [ConNF.Params] : Cardinal.mk ConNF.Litter = Cardinal.mk ConNF.μ

There are precisely μ litters.