Mathlib Map

Theorems · Definition · combinatorics

Set.Infinite

{α : Type u} → Set α → Prop

A set is infinite if it is not finite. This is protected so that it does not conflict with global Infinite.

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

Around this declaration

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

Set.Infinite.mono · cited by 25Infinite.monoSet.finite_or_infinite · cited by 23Set.finite_or_infiniteCardinal.lt_aleph0 · cited by 19Cardinal.lt_aleph0Set.Infinite.to_subtype · cited by 19Infinite.to_subtypeSet.infinite_coe_iff · cited by 16Set.infinite_coe_ifffinprod_of_infinite_mulSupport · cited by 13finprod_of_infinite_mulSu…Set.infinite_univ · cited by 13Set.infinite_univSet.Infinite.ncard · cited by 12Infinite.ncardSet.Infinite.natEmbedding · cited by 10Infinite.natEmbeddingSet.Infinite.sdiff · cited by 10Infinite.sdifffinsum_of_infinite_support · cited by 10finsum_of_infinite_supportNat.nth_mem · cited by 9Nat.nth_memSet.infinite_range_of_injective · cited by 9Set.infinite_range_of_inj…Set.infinite_image_iff · cited by 7Set.infinite_image_iffSet.not_infinite · cited by 7Set.not_infiniteSet · cited by 53352SetSet.Finite · cited by 1814Set.FiniteSet.InfiniteCITED BYCITES

Cites2

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.Finiteproof · cited by 1,814

Cited by267

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 267.