Mathlib Map

Theorems · Theorem · combinatorics

Set.toFinite

∀ {α : Type u} (s : Set α) [Finite ↑s], s.Finite

Constructor for Set.Finite using a Finite instance.

Defined in
Mathlib.Data.Finite.Defs
Cited by
174 results in Mathlib
Foundations
Depth 6 from the axioms, rests on 10 definitions · uses no axioms
Assumes
Finite
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.finite_toSet · cited by 210Finset.finite_toSetSet.Finite.image · cited by 96Finite.imageSet.Finite.union · cited by 74Finite.unionSet.finite_singleton · cited by 70Set.finite_singletonSet.finite_range · cited by 58Set.finite_rangeSet.finite_univ · cited by 52Set.finite_univSet.Finite.induction_on · cited by 39Finite.induction_onSet.finite_empty · cited by 26Set.finite_emptySet.finite_le_nat · cited by 16Set.finite_le_natSet.Finite.image2 · cited by 16Finite.image2Set.ncard_coe_finset · cited by 15Set.ncard_coe_finsetisOfFinOrder_of_finite · cited by 14isOfFinOrder_of_finiteSet.ncard_empty · cited by 14Set.ncard_emptySet.finite_iUnion · cited by 14Set.finite_iUnionSet.finite_Icc · cited by 13Set.finite_IccSet · cited by 53352SetSet.Elem · cited by 7166Set.ElemFinite · cited by 3029FiniteSet.Finite · cited by 1814Set.FiniteSet.toFiniteCITED BYCITES

Cites4

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
  • Set.Elemstatement and proof · cited by 7,166
  • Finitestatement and proof · cited by 3,029
  • Set.Finitestatement · cited by 1,814

Cited by174

Results whose statement or proof uses this declaration.