Mathlib Map

Theorems · Theorem · combinatorics

Set.Sized.mono

∀ {α : Type u_1} {A B : Set (Finset α)} {r : ℕ}, A ⊆ B → Set.Sized r B → Set.Sized r A
Defined in
Mathlib.Data.Finset.Slice
Cited by
2 results in Mathlib
Foundations
Depth 14 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.sized_union · cited by 2Set.sized_unionFinset.kruskal_katona · cited by 1Finset.kruskal_katonaSet · cited by 53352SetFinset · cited by 13712FinsetSet.Sized · cited by 35Set.SizedSized.monoCITED BYCITES

Cites3

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

  • Setstatement and proof · cited by 53,352
  • Finsetstatement and proof · cited by 13,712
  • Set.Sizedstatement and proof · cited by 35

Cited by2

Results whose statement or proof uses this declaration.