Theorems · Theorem · order theory
Set.not_nontrivial_iff
∀ {α : Type u} {s : Set α}, ¬s.Nontrivial ↔ s.Subsingleton- Defined in
- Mathlib.Data.Set.Subsingleton
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.Subsingletonstatement · cited by 276
- Set.Nontrivialstatement · cited by 145
- Iff.not_leftproof · cited by 49
- Set.not_subsingleton_iffproof · cited by 7
Cited by13
Results whose statement or proof uses this declaration.
- Set.einfsep_pos_of_finiteproof · cited by 4
- Finset.coe_infsepproof · cited by 2
- Set.infsep_eq_iInfproof · cited by 1
- Set.le_edist_of_le_infsepproof · cited by 1
- Set.Subsingleton.not_nontrivialproof · cited by 1
- Set.infsep_of_fintypeproof · cited by 1
- Set.Finite.infsepproof · cited by 1
- Set.offDiag_eq_emptyproof · cited by 1
- SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingletonproof · cited by 1
- Set.nontrivial_of_infsep_posproof · cited by 0
- SimpleGraph.Subgraph.Preconnected.degree_zero_iffproof · cited by 0
- isTotallyDisconnected_iff_ltproof · cited by 0