PFR/Mathlib/Data/Finset/Basic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. lemma Finset.ne_empty_iff_nonempty line 10 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Iff, Ne, EmptyCollection.emptyCollection, Finset.Nonempty

    Proof uses: Iff.symm, Finset.nonempty_iff_ne_empty

    2 instances, coercions and auxiliary constants left out.