Reference · Finite sets

rainbow.math.sets.finset.data

Finite sets src/rainbow/math/sets/finset/data.clj10 definitions, 6 theorems

Computational finite sets: duplicate-free enumerations paired with proof data. The older `finset/Finset` is deliberately extensional and therefore cannot eliminate its propositional cover into executable data. This representation keeps the enumeration in Type, carries duplicate-freedom in Prop, and projects to the extensional representation without changing the kernel.

list/no-duplicates

DefinitionSource, line 73

list/no-duplicates.{u} :
  (A : Type u) (x₁ : List A)
  → Prop

List = data/List

finset-data/Finset

DefinitionSource, line 97

finset-data/Finset.{u} :
  (A : Type u)
  → Type u

finset-data/enumeration

DefinitionSource, line 113

finset-data/enumeration.{u} :
  (A : Type u) (source : Finset A)
  → List A

Finset = finset-data/FinsetList = data/List

finset-data/duplicate-free

DefinitionSource, line 133

finset-data/duplicate-free.{u} :
  (A : Type u) (source : Finset A)
  → list/no-duplicates A (finset-data/enumeration A source)

Finset = finset-data/Finset

finset-data/to-set

DefinitionSource, line 153

finset-data/to-set.{u} :
  (A : Type u) (source : Finset A)
  → set/Set A

Finset = finset-data/Finset

finset-data/to-extensional

DefinitionSource, line 189

finset-data/to-extensional.{u} :
  (A : Type u) (source : Finset A)
  → finset/Finset A

Finset = finset-data/Finset

finset-data/card

DefinitionSource, line 205

finset-data/card.{u} :
  (A : Type u) (source : Finset A)
  → ℕ

Finset = finset-data/Finsetℕ = data/Nat

list/nat-sum

DefinitionSource, line 219

list/nat-sum :
  (x₁ : List ℕ)
  → ℕ

List = data/Listℕ = data/Nat

finset-data/sum-nat

DefinitionSource, line 238

finset-data/sum-nat :
  (x₁ : Finset ℕ)
  → ℕ

Finset = finset-data/Finsetℕ = data/Nat

finset-data/range

DefinitionSource, line 395

finset-data/range :
  (x₁ : ℕ)
  → Finset ℕ

Finset = finset-data/Finsetℕ = data/Nat

nat/member-range-below

TheoremFor all inputsNo axiomsSource, line 264

nat/member-range-below :
  (upper value : ℕ) (member : list/membership ℕ (list/nat-range upper) value)
  → nat/strict-below value upper

ℕ = data/Nat

list/nat-range-no-duplicates

TheoremFor all inputsNo axiomsSource, line 360

list/nat-range-no-duplicates :
  (upper : ℕ)
  → list/no-duplicates ℕ (list/nat-range upper)

ℕ = data/Nat

finset-data/enumeration-sound

TheoremFor all inputsNo axiomsSource, line 419

finset-data/enumeration-sound.{u} :
  (A : Type u) (source : Finset A) (value : A)
  (member : list/membership A (finset-data/enumeration A source) value)
  → value ∈ source

Finset = finset-data/Finset∈ = finset-data/to-set: membership in a finite set

finset-data/enumeration-complete

TheoremFor all inputsNo axiomsSource, line 437

finset-data/enumeration-complete.{u} :
  (A : Type u) (source : Finset A) (value : A)
  (member : value ∈ source)
  → list/membership A (finset-data/enumeration A source) value

Finset = finset-data/Finset∈ = finset-data/to-set: membership in a finite set

finset-data/sum-nat-enumeration

TheoremHolds by unfolding a definitionNo axiomsSource, line 461

finset-data/sum-nat-enumeration :
  (source : Finset ℕ)
  → finset-data/sum-nat source = list/nat-sum (finset-data/enumeration ℕ source)

= = equality/EqFinset = finset-data/Finsetℕ = data/Nat

finset-data/card-range

TheoremFor all inputsNo axiomsSource, line 484

finset-data/card-range :
  (upper : ℕ)
  → finset-data/card ℕ (finset-data/range upper) = upper

= = equality/Eqℕ = data/Nat