Principal upper/lower sets #
The results in this file all assume that the underlying type is equipped with at least a preorder.
Main declarations #
UpperSet.Ici
: Principal upper set.Set.Ici
as an upper set.UpperSet.Ioi
: Strict principal upper set.Set.Ioi
as an upper set.LowerSet.Iic
: Principal lower set.Set.Iic
as a lower set.LowerSet.Iio
: Strict principal lower set.Set.Iio
as a lower set.
Principal upper set. Set.Ici
as an upper set. The smallest upper set containing a given
element.
Equations
- UpperSet.Ici a = { carrier := Set.Ici a, upper' := ⋯ }
Instances For
Strict principal upper set. Set.Ioi
as an upper set.
Equations
- UpperSet.Ioi a = { carrier := Set.Ioi a, upper' := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
theorem
UpperSet.Ici_iSup₂
{α : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[CompleteLattice α]
(f : (i : ι) → κ i → α)
:
Principal lower set. Set.Iic
as a lower set. The smallest lower set containing a given
element.
Equations
- LowerSet.Iic a = { carrier := Set.Iic a, lower' := ⋯ }
Instances For
Strict principal lower set. Set.Iio
as a lower set.
Equations
- LowerSet.Iio a = { carrier := Set.Iio a, lower' := ⋯ }
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
theorem
LowerSet.Iic_iInf₂
{α : Type u_1}
{ι : Sort u_3}
{κ : ι → Sort u_4}
[CompleteLattice α]
(f : (i : ι) → κ i → α)
: