Mathlib Map

Theorems · Theorem · combinatorics

Set.Finite.to_subtype

∀ {α : Type u} {s : Set α}, s.Finite → Finite ↑s

Projection of Set.Finite to its Finite instance. This is intended to be used with dot notation. See also Set.Finite.Fintype and Set.Finite.nonempty_fintype.

Defined in
Mathlib.Data.Finite.Defs
Cited by
44 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.Finite.subset · cited by 285Finite.subsetSet.Finite.image · cited by 96Finite.imageSet.Finite.countable · cited by 30Finite.countableSet.Finite.of_finite_image · cited by 20Finite.of_finite_imageSet.Finite.image2 · cited by 16Finite.image2Set.Finite.prod · cited by 9Finite.prodSupClosed.sSup_mem · cited by 5SupClosed.sSup_memSet.finite_subset_iUnion · cited by 4Set.finite_subset_iUnionSet.Finite.biUnion' · cited by 4Finite.biUnion'InfClosed.sInf_mem · cited by 4InfClosed.sInf_memTopology.IsLower.isTopologicalBasis · cited by 3IsLower.isTopologicalBasisfour_functions_theorem · cited by 3four_functions_theoremAlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact · cited by 3AlgebraicGeometry.exists_…IsSemisimpleModule.finite_tfae · cited by 2IsSemisimpleModule.finite…AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat · cited by 2AlgebraicGeometry.mono_pu…Set · cited by 53352SetSet.Elem · cited by 7166Set.ElemFinite · cited by 3029FiniteSet.Finite · cited by 1814Set.FiniteFinite.to_subtypeCITED 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 · cited by 7,166
  • Finitestatement · cited by 3,029
  • Set.Finitestatement and proof · cited by 1,814

Cited by44

Results whose statement or proof uses this declaration.