The complete lattice structure on UpperSet
/LowerSet
#
This file defines a completely distributive lattice structure on UpperSet
and LowerSet
,
pulled back across the canonical injection (UpperSet.carrier
, LowerSet.carrier
) into Set α
.
Notes #
Upper sets are ordered by reverse inclusion. This convention is motivated by the fact that this
makes them order-isomorphic to lower sets and antichains, and matches the convention on Filter
.
@[simp]
@[simp]
Equations
Equations
@[deprecated UpperSet.notMem_top (since := "2025-05-23")]
Alias of UpperSet.notMem_top
.
@[simp]
Equations
Equations
@[deprecated LowerSet.notMem_bot (since := "2025-05-23")]
Alias of LowerSet.notMem_bot
.
Complement #
@[simp]
@[simp]
noncomputable instance
UpperSet.instLinearOrder
{α : Type u_1}
[LinearOrder α]
:
LinearOrder (UpperSet α)
Equations
noncomputable instance
LowerSet.instLinearOrder
{α : Type u_1}
[LinearOrder α]
:
LinearOrder (LowerSet α)
Equations
Equations
Equations
@[simp]
@[simp]