rainbow.math.logic.fintype

fintype/Fintype

DefinitionSource, line 76

fintype/Fintype.{u} :
  (A : Type u)
  → Type u

fintype/elements

DefinitionSource, line 88

fintype/elements.{u} :
  (A : Type u) (instance : fintype/Fintype A)
  → finset/Finset A

fintype/complete

DefinitionSource, line 102

fintype/complete.{u} :
  (A : Type u) (instance : fintype/Fintype A) (value : A)
  → finset/to-set A (fintype/elements A instance) value

fintype/from-finite

TheoremFor all inputsNo axiomsSource, line 127

fintype/from-finite.{u} :
  (A : Type u) (finite-evidence : type/finite A)
  → fintype/Fintype A

fintype/to-finite

TheoremFor all inputsNo axiomsSource, line 153

fintype/to-finite.{u} :
  (A : Type u) (instance : fintype/Fintype A)
  → type/finite A

fintype/subsingleton

TheoremFor all inputsAxioms: sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 178

fintype/subsingleton.{u} :
  (A : Type u)
  → type/subsingleton (fintype/Fintype A)

fintype/finite-equivalent-nonempty

TheoremFor all inputsNo axiomsSource, line 211

fintype/finite-equivalent-nonempty.{u} :
  (A : Type u)
  → proposition/conjunction (type/finite A → proposition/nonempty (fintype/Fintype A)) (proposition/nonempty (fintype/Fintype A) → type/finite A)

fintype/is-empty-equivalent-infinite

TheoremFor all inputsNo axiomsSource, line 242

fintype/is-empty-equivalent-infinite.{u} :
  (A : Type u)
  → proposition/conjunction (proposition/is-empty (fintype/Fintype A) → type/infinite A) (type/infinite A → proposition/is-empty (fintype/Fintype A))

fintype/infinite-of-is-empty

TheoremFor all inputsNo axiomsSource, line 270

fintype/infinite-of-is-empty.{u} :
  (A : Type u) (empty : proposition/is-empty (fintype/Fintype A))
  → type/infinite A

fintype/is-empty-proposition-equality

TheoremFor all inputsAxioms: sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 287

fintype/is-empty-proposition-equality.{u} :
  (A : Type u)
  → proposition/is-empty (fintype/Fintype A) = type/infinite A

= = equality/Eq

set/finite-to-nonempty-fintype

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7Source, line 309

set/finite-to-nonempty-fintype.{u} :
  (A : Type u) (source : set/Set A) (finite-evidence : set/finite A source)
  → proposition/nonempty (fintype/Fintype (data/Subtype A source))

set/universal-finite-equivalent-nonempty-fintype

TheoremFor all inputsNo axiomsSource, line 337

set/universal-finite-equivalent-nonempty-fintype.{u} :
  (A : Type u)
  → proposition/conjunction (set/finite A (set/universal A) → proposition/nonempty (fintype/Fintype A)) (proposition/nonempty (fintype/Fintype A) → set/finite A (set/universal A))

set/finite-equivalent-subtype-fintype

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7Source, line 376

set/finite-equivalent-subtype-fintype.{u} :
  (A : Type u) (source : set/Set A)
  → proposition/conjunction (set/finite A source → proposition/nonempty (fintype/Fintype (data/Subtype A source))) (proposition/nonempty (fintype/Fintype (data/Subtype A source)) → set/finite A source)