Theorems · Theorem
Equiv.subsingleton
∀ {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton β], Subsingleton α- Defined in
- Mathlib.Logic.Equiv.Defs
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses Quot.sound
- Assumes
- Subsingleton
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement and proof · cited by 8,337
- Equiv.injectiveproof · cited by 464
- Function.Injective.subsingletonproof · cited by 16
Cited by24
Results whose statement or proof uses this declaration.
- Equiv.subsingleton_congrproof · cited by 28
- AddCommGrpCat.subsingleton_of_isZeroproof · cited by 4
- CategoryTheory.HasProjectiveDimensionLT.subsingletonproof · cited by 3
- Subalgebra.eq_bot_of_rank_le_oneproof · cited by 3
- IsIsotypic.linearEquiv_funproof · cited by 3
- Subalgebra.rank_eq_one_iffproof · cited by 3
- CategoryTheory.HasProjectiveDimensionLT.mkproof · cited by 2
- IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimesproof · cited by 2
- Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlatproof · cited by 2
- Module.subsingleton_of_rank_zeroproof · cited by 2
- CategoryTheory.HasInjectiveDimensionLT.mkproof · cited by 2