Theorems · Definition · order theory
SupIrred
{α : Type u_2} → [SemilatticeSup α] → α → PropA sup-irreducible element is a non-bottom element which isn't the supremum of anything smaller.
- Defined in
- Mathlib.Order.Irreducible
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- SemilatticeSup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SemilatticeSupstatement and proof · cited by 785
- IsMinproof · cited by 277
Cited by41
Results whose statement or proof uses this declaration.
- OrderEmbedding.birkhoffSetstatement and proof · cited by 6
- OrderEmbedding.birkhoffFinsetstatement and proof · cited by 4
- LowerSet.supIrred_Iicstatement · cited by 4
- OrderIso.lowerSetSupIrredstatement and proof · cited by 3
- OrderIso.supIrredLowerSetstatement · cited by 3
- OrderEmbedding.supIrredLowerSetstatement · cited by 2
- not_supIrredstatement · cited by 2
- SupIrred.ne_botstatement and proof · cited by 2
- LatticeHom.birkhoffFinsetstatement and proof · cited by 2
- not_supIrred_botstatement · cited by 1
- OrderEmbedding.birkhoffSet_infstatement and proof · cited by 1
- OrderEmbedding.birkhoffSet_supstatement and proof · cited by 1