Theorems · Definition · order theory
UpperSet.erase
{α : Type u_1} → [inst : Preorder α] → UpperSet α → α → UpperSet αThe biggest upper subset of an upper set s not containing an element a.
- Defined in
- Mathlib.Order.UpperLower.Closure
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 12 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.
- SetLike.coeproof · cited by 8,199
- Preorderstatement and proof · cited by 7,952
- UpperSetstatement and proof · cited by 245
- LowerSet.Iicproof · cited by 37
Cited by9
Results whose statement or proof uses this declaration.
- UpperSet.sdiff_singletonstatement · cited by 2
- UpperSet.erase_inf_Icistatement and proof · cited by 2
- UpperSet.le_erasestatement · cited by 1
- UpperSet.lt_erasestatement · cited by 1
- UpperSet.infIrred_iff_of_finiteproof · cited by 1
- UpperSet.erase_eqstatement · cited by 1
- UpperSet.Ici_inf_erasestatement and proof · cited by 0
- UpperSet.coe_erasestatement · cited by 0
- UpperSet.erase_idemstatement and proof · cited by 0