Theorems · Definition · order theory
LowerSet.Iic
{α : Type u_1} → [inst : Preorder α] → α → LowerSet αPrincipal lower set. Set.Iic as a lower set. The smallest lower set containing a given
element.
- Defined in
- Mathlib.Order.UpperLower.Principal
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Set.Iicproof · cited by 1,111
- LowerSetstatement · cited by 230
- isLowerSet_Iicproof · cited by 8
Cited by42
Results whose statement or proof uses this declaration.
- Order.Ideal.principalproof · cited by 12
- UpperSet.eraseproof · cited by 9
- lowerClosure_singletonstatement · cited by 8
- LowerSet.supIrred_Iicstatement and proof · cited by 4
- LowerSet.mem_Iic_iffstatement · cited by 3
- Topology.IsUpperSet.closure_singletonproof · cited by 3
- OrderEmbedding.supIrredLowerSetproof · cited by 2
- LowerSet.Iic_ne_botstatement · cited by 2
- LowerSet.coe_Iicstatement · cited by 2
- LowerSet.erase_sup_Iicstatement · cited by 2
- LowerSet.iicsInfHomproof · cited by 2
- LowerSet.iicInfHomproof · cited by 2