Theorems · Theorem · order theory
LowerSet.supIrred_Iic
∀ {α : Type u_1} [inst : PartialOrder α] (a : α), SupIrred (LowerSet.Iic a)- Defined in
- Mathlib.Order.Birkhoff
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- le_reflproof · cited by 2,061
- LE.le.antisymmproof · cited by 507
- LE.le.trans_eqproof · cited by 328
- IsMinproof · cited by 277
- le_sup_leftproof · cited by 265
- le_sup_rightproof · cited by 242
- LowerSetstatement and proof · cited by 230
- LowerSet.Iicstatement and proof · cited by 37
- SupIrredstatement · cited by 34
- IsMin.eq_botproof · cited by 12
- LowerSet.mem_Iic_iffproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- OrderEmbedding.supIrredLowerSetproof · cited by 2
- LowerSet.supIrred_iff_of_finiteproof · cited by 1
- OrderEmbedding.supIrredLowerSet_applystatement · cited by 0
- OrderEmbedding.supIrredLowerSet_surjectiveproof · cited by 0
- OrderIso.supIrredLowerSet_applystatement · cited by 0