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.

@[implicit_reducible]

def UpperSet.Ici {α : Type u_1} [Preorder α] (a : α) : UpperSet α

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' := ⋯ }

@[implicit_reducible]

def LowerSet.Iic {α : Type u_1} [Preorder α] (a : α) : LowerSet α

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' := ⋯ }

@[implicit_reducible]

def UpperSet.Ioi {α : Type u_1} [Preorder α] (a : α) : UpperSet α

Strict principal upper set. Set.Ioi as an upper set.

Equations

• UpperSet.Ioi a = { carrier := Set.Ioi a, upper' := ⋯ }

@[implicit_reducible]

def LowerSet.Iio {α : Type u_1} [Preorder α] (a : α) : LowerSet α

Strict principal lower set. Set.Iio as a lower set.

Equations

• LowerSet.Iio a = { carrier := Set.Iio a, lower' := ⋯ }

@[simp]

theorem UpperSet.coe_Ici {α : Type u_1} [Preorder α] (a : α) : ↑(Ici a) = Set.Ici a

@[simp]

theorem LowerSet.coe_Iic {α : Type u_1} [Preorder α] (a : α) : ↑(Iic a) = Set.Iic a

@[simp]

theorem UpperSet.coe_Ioi {α : Type u_1} [Preorder α] (a : α) : ↑(Ioi a) = Set.Ioi a

@[simp]

theorem LowerSet.coe_Iio {α : Type u_1} [Preorder α] (a : α) : ↑(Iio a) = Set.Iio a

@[simp]

theorem UpperSet.mem_Ici_iff {α : Type u_1} [Preorder α] {a b : α} : b ∈ Ici a ↔ a ≤ b

@[simp]

theorem LowerSet.mem_Iic_iff {α : Type u_1} [Preorder α] {a b : α} : b ∈ Iic a ↔ b ≤ a

@[simp]

theorem UpperSet.mem_Ioi_iff {α : Type u_1} [Preorder α] {a b : α} : b ∈ Ioi a ↔ a < b

@[simp]

theorem LowerSet.mem_Iio_iff {α : Type u_1} [Preorder α] {a b : α} : b ∈ Iio a ↔ b < a

@[simp]

theorem UpperSet.map_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) : (map f) (Ici a) = Ici (f a)

@[simp]

theorem LowerSet.map_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) : (map f) (Iic a) = Iic (f a)

@[simp]

theorem UpperSet.map_Ioi {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) : (map f) (Ioi a) = Ioi (f a)

@[simp]

theorem LowerSet.map_Iio {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (a : α) : (map f) (Iio a) = Iio (f a)

theorem UpperSet.Ici_le_Ioi {α : Type u_1} [Preorder α] (a : α) : Ici a ≤ Ioi a

theorem LowerSet.Ioi_le_Ici {α : Type u_1} [Preorder α] (a : α) : Iio a ≤ Iic a

@[simp]

theorem UpperSet.Ici_bot {α : Type u_1} [Preorder α] [OrderBot α] : Ici ⊥ = ⊥

@[simp]

theorem LowerSet.Iic_top {α : Type u_1} [Preorder α] [OrderTop α] : Iic ⊤ = ⊤

@[simp]

theorem UpperSet.Ioi_top {α : Type u_1} [Preorder α] [OrderTop α] : Ioi ⊤ = ⊤

@[simp]

theorem LowerSet.Iio_bot {α : Type u_1} [Preorder α] [OrderBot α] : Iio ⊥ = ⊥

@[simp]

theorem UpperSet.Ici_ne_top {α : Type u_1} [Preorder α] {a : α} : Ici a ≠ ⊤

@[simp]

theorem LowerSet.Iic_ne_bot {α : Type u_1} [Preorder α] {a : α} : Iic a ≠ ⊥

@[simp]

theorem UpperSet.Ici_lt_top {α : Type u_1} [Preorder α] {a : α} : Ici a < ⊤

@[simp]

theorem LowerSet.bot_lt_Iic {α : Type u_1} [Preorder α] {a : α} : ⊥ < Iic a

@[simp]

theorem UpperSet.le_Ici {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} : s ≤ Ici a ↔ a ∈ s

@[simp]

theorem LowerSet.Iic_le {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} : Iic a ≤ s ↔ a ∈ s

theorem UpperSet.Ici_strictMono (α : Type u_1) [Preorder α] : StrictMono Ici

theorem LowerSet.Iic_strictMono (α : Type u_1) [Preorder α] : StrictMono Iic

theorem UpperSet.Ioi_strictMono (α : Type u_1) [Preorder α] : StrictMono Ioi

theorem LowerSet.Iio_strictMono (α : Type u_1) [Preorder α] : StrictMono Iio

theorem UpperSet.Ici_injective {α : Type u_1} [PartialOrder α] : Function.Injective Ici

theorem LowerSet.Iic_injective {α : Type u_1} [PartialOrder α] : Function.Injective Iic

@[simp]

theorem UpperSet.Ici_inj {α : Type u_1} [PartialOrder α] {a b : α} : Ici a = Ici b ↔ a = b

@[simp]

theorem LowerSet.Iic_inj {α : Type u_1} [PartialOrder α] {a b : α} : Iic a = Iic b ↔ a = b

theorem UpperSet.Ici_ne_Ici {α : Type u_1} [PartialOrder α] {a b : α} : Ici a ≠ Ici b ↔ a ≠ b

theorem LowerSet.Iic_ne_Iic {α : Type u_1} [PartialOrder α] {a b : α} : Iic a ≠ Iic b ↔ a ≠ b

@[simp]

theorem UpperSet.Ioi_eq_top {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} : Ioi a = ⊤ ↔ a = ⊤

@[simp]

theorem LowerSet.Iio_eq_bot {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} : Iio a = ⊥ ↔ a = ⊥

@[simp]

theorem UpperSet.Ici_sup {α : Type u_1} [SemilatticeSup α] (a b : α) : Ici (a ⊔ b) = Ici a ⊔ Ici b

@[simp]

theorem LowerSet.Iic_inf {α : Type u_1} [SemilatticeInf α] (a b : α) : Iic (a ⊓ b) = Iic a ⊓ Iic b

@[simp]

theorem UpperSet.Ici_sSup {α : Type u_1} [CompleteLattice α] (S : Set α) : Ici (sSup S) = ⨆ a ∈ S, Ici a

@[simp]

theorem LowerSet.Iic_sInf {α : Type u_1} [CompleteLattice α] (S : Set α) : Iic (sInf S) = ⨅ a ∈ S, Iic a

@[simp]

theorem UpperSet.Ici_iSup {α : Type u_1} {ι : Sort u_3} [CompleteLattice α] (f : ι → α) : Ici (⨆ (i : ι), f i) = ⨆ (i : ι), Ici (f i)

@[simp]

theorem LowerSet.Iic_iInf {α : Type u_1} {ι : Sort u_3} [CompleteLattice α] (f : ι → α) : Iic (⨅ (i : ι), f i) = ⨅ (i : ι), Iic (f i)

theorem UpperSet.Ici_iSup₂ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [CompleteLattice α] (f : (i : ι) → κ i → α) : Ici (⨆ (i : ι), ⨆ (j : κ i), f i j) = ⨆ (i : ι), ⨆ (j : κ i), Ici (f i j)

theorem LowerSet.Iic_iInf₂ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [CompleteLattice α] (f : (i : ι) → κ i → α) : Iic (⨅ (i : ι), ⨅ (j : κ i), f i j) = ⨅ (i : ι), ⨅ (j : κ i), Iic (f i j)