Mathlib Map

Theorems · Theorem · combinatorics

Finset.dens_eq_one

∀ {α : Type u_2} [inst : Fintype α] {s : Finset α} [Nonempty α], s.dens = 1 ↔ s = Finset.univ
Defined in
Mathlib.Data.Finset.Density
Cited by
1 results in Mathlib
Foundations
Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FintypeNonempty
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Finset.dens_ne_one · cited by 0Finset.dens_ne_oneFinset · cited by 13712FinsetFintype · cited by 7736FintypeFinset.univ · cited by 3473Finset.univNNRat · cited by 523NNRatFinset.dens · cited by 55Finset.densFinset.dens_eq_oneCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Finsetstatement and proof · cited by 13,712
  • Fintypestatement and proof · cited by 7,736
  • Finset.univstatement and proof · cited by 3,473
  • NNRatstatement · cited by 523
  • Finset.densstatement · cited by 55

Cited by1

Results whose statement or proof uses this declaration.