Documentation

ConNF.External.Counting

New file #

In this file...

Main declarations #

source
def ConNF.insert [ConNF.Params] {α : ConNF.Λ} (x : ConNF.TSet ↑α) :
ConNF.TSet ↑α

The set {z ∪ {a} | z ∈ x}.

Equations
Instances For
    source
    def ConNF.cardinalNat [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (n : ℕ) :
    ConNF.TSet ↑α
    Equations
    Instances For
      source
      @[simp]
      theorem ConNF.mem_cardinalNat_iff [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (n : ℕ) (a : ConNF.TSet ↑β) :
      a ∈[hβ] ConNF.cardinalNat hβ hγ n ↔ ∃ (s : Finset (ConNF.TSet ↑γ)), s.card = n ∧ ∀ (b : ConNF.TSet ↑γ), b ∈[hγ] a ↔ b ∈ s