Mathlib Map

Theorems · Theorem · combinatorics

Set.finite_coe_iff

∀ {α : Type u} {s : Set α}, Finite ↑s ↔ s.Finite
Defined in
Mathlib.Data.Finite.Defs
Cited by
21 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.infinite_coe_iff · cited by 16Set.infinite_coe_iffCardinal.lt_aleph0_iff_set_finite · cited by 7Cardinal.lt_aleph0_iff_se…Ideal.finite_factors · cited by 7Ideal.finite_factorsIsCompact.finite · cited by 5IsCompact.finiteSet.not_injOn_infinite_finite_image · cited by 4Set.not_injOn_infinite_fi…finite_zmultiples · cited by 3finite_zmultiplesfinite_memPartition · cited by 3finite_memPartitionNumberField.hermiteTheorem.finite_of_finite_generating_set · cited by 2hermiteTheorem.finite_of_…Finset.card_preimage_eq_sum_card_image_eq · cited by 1Finset.card_preimage_eq_s…MeasureTheory.mem_generateSetAlgebra_elim · cited by 1MeasureTheory.mem_generat…IsCyclotomicExtension.finite · cited by 1IsCyclotomicExtension.fin…LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo · cited by 1LinearEquiv.isOfFinOrder_…Set.Finite.injOn_iff_bijOn_of_mapsTo · cited by 1Finite.injOn_iff_bijOn_of…Set.card_union_le · cited by 1Set.card_union_lefinite_of_fin_dim_affineIndependent · cited by 1finite_of_fin_dim_affineI…Set · cited by 53352SetSet.Elem · cited by 7166Set.ElemFinite · cited by 3029FiniteSet.Finite · cited by 1814Set.FiniteSet.finite_coe_iffCITED 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 · cited by 1,814

Cited by21

Results whose statement or proof uses this declaration.