Mathlib Map

Theorems · Theorem · combinatorics

Set.infinite_or_finite

∀ {α : Type u} (s : Set α), s.Infinite ∨ s.Finite
Defined in
Mathlib.Data.Finite.Defs
Cited by
6 results in Mathlib
Foundations
Depth 12 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set.ncard_sdiff_singleton_of_mem · cited by 2Set.ncard_sdiff_singleton…Set.exists_union_disjoint_cardinal_eq_of_even · cited by 2Set.exists_union_disjoint…Set.exists_subsuperset_card_eq · cited by 1Set.exists_subsuperset_ca…finsum_one · cited by 1finsum_oneSet.natCard_add_le · cited by 1Set.natCard_add_leSet.natCard_mul_le · cited by 1Set.natCard_mul_leSet · cited by 53352SetSet.Finite · cited by 1814Set.FiniteSet.Infinite · cited by 263Set.Infiniteem' · cited by 12em'Set.infinite_or_finiteCITED 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.Finitestatement and proof · cited by 1,814
  • Set.Infinitestatement · cited by 263
  • em'proof · cited by 12

Cited by6

Results whose statement or proof uses this declaration.