Theorems · Definition · order theory

Set.Nontrivial

{α : Type u} → Set α → Prop

A set s is Set.Nontrivial if it has at least two distinct elements.

Defined in: Mathlib.Data.Set.Subsingleton
Cited by: 145 results in Mathlib
Foundations: Depth 4 from the axioms, rests on 13 definitions · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites1

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

Cited by148

Results whose statement or proof uses this declaration.

Finset.Nontrivialproof · cited by 53
Set.not_nontrivial_iffstatement · cited by 13
Set.Nontrivial.nonemptystatement and proof · cited by 10
Set.subsingleton_or_nontrivialstatement · cited by 9
Set.Nontrivial.exists_nestatement and proof · cited by 8
Set.not_subsingleton_iffstatement · cited by 7
Set.Nontrivial.le_infsep_iffstatement and proof · cited by 6
Set.nontrivial_coe_sortstatement · cited by 6
Set.eq_singleton_or_nontrivialstatement and proof · cited by 5
Set.Nontrivial.not_subset_singletonstatement and proof · cited by 5
Set.Nontrivial.not_subsingletonstatement · cited by 5
Set.offDiag_nonemptystatement · cited by 4