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
.
Equations
- UpperSet.instSetLike = { coe := UpperSet.carrier, coe_injective' := ⋯ }
@[simp]
@[simp]
Equations
- LowerSet.instSetLike = { coe := LowerSet.carrier, coe_injective' := ⋯ }
@[simp]
@[simp]
Equations
- UpperSet.instMax = { max := fun (s t : UpperSet α) => { carrier := ↑s ∩ ↑t, upper' := ⋯ } }
Equations
- UpperSet.instMin = { min := fun (s t : UpperSet α) => { carrier := ↑s ∪ ↑t, upper' := ⋯ } }
Equations
- UpperSet.instTop = { top := { carrier := ∅, upper' := ⋯ } }
Equations
- UpperSet.instBot = { bot := { carrier := Set.univ, upper' := ⋯ } }
Equations
- UpperSet.instSupSet = { sSup := fun (S : Set (UpperSet α)) => { carrier := ⋂ s ∈ S, ↑s, upper' := ⋯ } }
Equations
- UpperSet.instInfSet = { sInf := fun (S : Set (UpperSet α)) => { carrier := ⋃ s ∈ S, ↑s, upper' := ⋯ } }
Equations
- UpperSet.completeLattice = Function.Injective.completeLattice (⇑OrderDual.toDual ∘ SetLike.coe) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- UpperSet.instInhabited = { default := ⊥ }
@[simp]
Equations
- LowerSet.instMax = { max := fun (s t : LowerSet α) => { carrier := ↑s ∪ ↑t, lower' := ⋯ } }
Equations
- LowerSet.instMin = { min := fun (s t : LowerSet α) => { carrier := ↑s ∩ ↑t, lower' := ⋯ } }
Equations
- LowerSet.instTop = { top := { carrier := Set.univ, lower' := ⋯ } }
Equations
- LowerSet.instBot = { bot := { carrier := ∅, lower' := ⋯ } }
Equations
- LowerSet.instSupSet = { sSup := fun (S : Set (LowerSet α)) => { carrier := ⋃ s ∈ S, ↑s, lower' := ⋯ } }
Equations
- LowerSet.instInfSet = { sInf := fun (S : Set (LowerSet α)) => { carrier := ⋂ s ∈ S, ↑s, lower' := ⋯ } }
Equations
Equations
- One or more equations did not get rendered due to their size.
Equations
- LowerSet.instInhabited = { default := ⊥ }
Complement #
Upper sets are order-isomorphic to lower sets under complementation.
Equations
- upperSetIsoLowerSet = { toFun := UpperSet.compl, invFun := LowerSet.compl, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
Instances For
@[simp]
@[simp]
noncomputable instance
UpperSet.instLinearOrder
{α : Type u_1}
[LinearOrder α]
:
LinearOrder (UpperSet α)
Equations
noncomputable instance
LowerSet.instLinearOrder
{α : Type u_1}
[LinearOrder α]
:
LinearOrder (LowerSet α)
Equations
@[simp]
@[simp]