rainbow.math.sets.finset.nontrivial

finset/nontrivial

DefinitionSource, line 49

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

finset/nontrivial-nonempty

TheoremFor all inputsNo axiomsSource, line 76

finset/nontrivial-nonempty.{u} :
  (A : Type u) (source : finset/Finset A) (evidence : finset/nontrivial A source)
  → finset/nonempty A source

finset/empty-not-nontrivial

TheoremFor all inputsNo axiomsSource, line 122

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

finset/singleton-not-nontrivial

TheoremFor all inputsNo axiomsSource, line 164

finset/singleton-not-nontrivial.{u} :
  (A : Type u) (selected : A) (x₁ : finset/nontrivial A (finset/singleton A selected))
  → proposition/falsity

finset/empty-nontrivial-proposition-equality

TheoremFor all inputsAxioms: sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 221

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

= = equality/Eq