rainbow.math.logic.finset

finset/Finset

DefinitionSource, line 81

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

finset/to-set

DefinitionSource, line 93

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

finset/finite-evidence

DefinitionSource, line 107

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

finset/empty

DefinitionSource, line 136

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

finset/subset

DefinitionSource, line 148

finset/subset.{u} :
  (A : Type u) (x₁ x₂ : finset/Finset A)
  → Prop

finset/nonempty

DefinitionSource, line 163

finset/nonempty.{u} :
  (A : Type u) (x₁ : finset/Finset A)
  → Prop

finset/singleton

DefinitionSource, line 199

finset/singleton.{u} :
  (A : Type u) (x₁ : A)
  → finset/Finset A

finset/subset-reflexive-explicit

TheoremFor all inputsNo axiomsSource, line 214

finset/subset-reflexive-explicit.{u} :
  (A : Type u) (source : finset/Finset A)
  → finset/subset A source source

finset/subset-reflexive-implicit

TheoremFor all inputsNo axiomsSource, line 227

finset/subset-reflexive-implicit.{u} :
  (A : Type u) (source : finset/Finset A)
  → finset/subset A source source

finset/empty-subset

TheoremFor all inputsNo axiomsSource, line 240

finset/empty-subset.{u} :
  (A : Type u) (source : finset/Finset A)
  → finset/subset A (finset/empty A) source

finset/empty-not-nonempty

TheoremFor all inputsNo axiomsSource, line 254

finset/empty-not-nonempty.{u} :
  (A : Type u) (x₁ : finset/nonempty A (finset/empty A))
  → proposition/falsity

finset/empty-nonempty-proposition-equality

TheoremFor all inputsAxioms: sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 277

finset/empty-nonempty-proposition-equality.{u} :
  (A : Type u)
  → finset/nonempty A (finset/empty A) = proposition/falsity

= = equality/Eq

finset/singleton-nonempty

TheoremFor all inputsNo axiomsSource, line 303

finset/singleton-nonempty.{u} :
  (A : Type u) (selected : A)
  → finset/nonempty A (finset/singleton A selected)

finset/nonempty-to-type

TheoremFor all inputsNo axiomsSource, line 319

finset/nonempty-to-type.{u} :
  (A : Type u) (source : finset/Finset A) (inhabited : finset/nonempty A source)
  → proposition/nonempty A

finset/extensional

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

finset/extensional.{u} :
  (A : Type u) (left right : finset/Finset A)
  (pointwise : ∀ (value : A), proposition/conjunction (finset/to-set A left value → finset/to-set A right value) (finset/to-set A right value → finset/to-set A left value))
  → left = right

= = equality/Eq

finset/eq-empty-or-nonempty

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 384

finset/eq-empty-or-nonempty.{u} :
  (A : Type u) (source : finset/Finset A)
  → proposition/disjunction (source = finset/empty A) (finset/nonempty A source)

= = equality/Eq

finset/nonempty-not-equal-empty

TheoremFor all inputsNo axiomsSource, line 431

finset/nonempty-not-equal-empty.{u} :
  (A : Type u) (source : finset/Finset A) (inhabited : finset/nonempty A source)
  (h₁ : source = finset/empty A)
  → proposition/falsity

= = equality/Eq

finset/nonempty-of-not-equal-empty

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 457

finset/nonempty-of-not-equal-empty.{u} :
  (A : Type u) (source : finset/Finset A)
  (not-empty : source = finset/empty A → proposition/falsity)
  → finset/nonempty A source

= = equality/Eq

finset/nonempty-equivalent-not-empty

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 484

finset/nonempty-equivalent-not-empty.{u} :
  (A : Type u) (source : finset/Finset A)
  → proposition/conjunction (finset/nonempty A source → source = finset/empty A → proposition/falsity) ((source = finset/empty A → proposition/falsity) → finset/nonempty A source)

= = equality/Eq

finset/is-empty-of-all-empty

TheoremFor all inputsNo axiomsSource, line 513

finset/is-empty-of-all-empty.{u} :
  (A : Type u)
  (all-empty : ∀ (source : finset/Finset A), source = finset/empty A)
  → proposition/is-empty A

= = equality/Eq

finset/singleton-injective

TheoremFor all inputsNo axiomsSource, line 535

finset/singleton-injective.{u} :
  (A : Type u) (left right : A)
  (same-image : (fun value => finset/singleton A value) left = (fun value => finset/singleton A value) right)
  → left = right

= = equality/Eq