Theorems · Theorem · order theory
Set.Subsingleton.finite
∀ {α : Type u} {s : Set α}, s.Subsingleton → s.Finite- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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 · cited by 1,814
- Set.Subsingletonstatement and proof · cited by 276
- Set.finite_singletonproof · cited by 70
- Set.finite_emptyproof · cited by 26
- Set.Subsingleton.induction_onproof · cited by 12
Cited by20
Results whose statement or proof uses this declaration.
- MvPowerSeries.isRestricted_monomialproof · cited by 4
- Set.Subsingleton.countableproof · cited by 4
- circleAverage_log_norm_sub_const_eq_log_radius_add_posLogproof · cited by 1
- Set.Subsingleton.mem_codiscreteWithinproof · cited by 1
- Set.Subsingleton.partiallyWellOrderedOnproof · cited by 1
- MeasureTheory.StronglyMeasurable.of_subsingleton_codproof · cited by 1
- Dense.exists_countable_dense_subset_no_bot_topproof · cited by 1
- Algebra.QuasiFiniteAt.of_isOpen_singletonproof · cited by 1
- Set.finite_isBotproof · cited by 1
- Set.finite_isTopproof · cited by 1
- HasFDerivWithinAt.of_subsingletonproof · cited by 1
- wellQuasiOrderedLE_iff_wellFoundedLTproof · cited by 1