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.

instance UpperSet.instSetLike {α : Type u_1} [LE α] : SetLike (UpperSet α) α

Equations

• UpperSet.instSetLike = { coe := UpperSet.carrier, coe_injective' := ⋯ }

def UpperSet.Simps.coe {α : Type u_1} [LE α] (s : UpperSet α) : Set α

See Note [custom simps projection].

Equations

• UpperSet.Simps.coe s = ↑s

theorem UpperSet.ext {α : Type u_1} [LE α] {s t : UpperSet α} : ↑s = ↑t → s = t

theorem UpperSet.ext_iff {α : Type u_1} [LE α] {s t : UpperSet α} : s = t ↔ ↑s = ↑t

@[simp]

theorem UpperSet.carrier_eq_coe {α : Type u_1} [LE α] (s : UpperSet α) : s.carrier = ↑s

@[simp]

theorem UpperSet.upper {α : Type u_1} [LE α] (s : UpperSet α) : IsUpperSet ↑s

@[simp]

theorem UpperSet.coe_mk {α : Type u_1} [LE α] (s : Set α) (hs : IsUpperSet s) : ↑{ carrier := s, upper' := hs } = s

@[simp]

theorem UpperSet.mem_mk {α : Type u_1} [LE α] {s : Set α} (hs : IsUpperSet s) {a : α} : a ∈ { carrier := s, upper' := hs } ↔ a ∈ s

instance LowerSet.instSetLike {α : Type u_1} [LE α] : SetLike (LowerSet α) α

Equations

• LowerSet.instSetLike = { coe := LowerSet.carrier, coe_injective' := ⋯ }

def LowerSet.Simps.coe {α : Type u_1} [LE α] (s : LowerSet α) : Set α

See Note [custom simps projection].

Equations

• LowerSet.Simps.coe s = ↑s

theorem LowerSet.ext {α : Type u_1} [LE α] {s t : LowerSet α} : ↑s = ↑t → s = t

theorem LowerSet.ext_iff {α : Type u_1} [LE α] {s t : LowerSet α} : s = t ↔ ↑s = ↑t

@[simp]

theorem LowerSet.carrier_eq_coe {α : Type u_1} [LE α] (s : LowerSet α) : s.carrier = ↑s

@[simp]

theorem LowerSet.lower {α : Type u_1} [LE α] (s : LowerSet α) : IsLowerSet ↑s

@[simp]

theorem LowerSet.coe_mk {α : Type u_1} [LE α] (s : Set α) (hs : IsLowerSet s) : ↑{ carrier := s, lower' := hs } = s

@[simp]

theorem LowerSet.mem_mk {α : Type u_1} [LE α] {s : Set α} (hs : IsLowerSet s) {a : α} : a ∈ { carrier := s, lower' := hs } ↔ a ∈ s

instance UpperSet.instMax {α : Type u_1} [LE α] : Max (UpperSet α)

Equations

• UpperSet.instMax = { max := fun (s t : UpperSet α) => { carrier := ↑s ∩ ↑t, upper' := ⋯ } }

instance UpperSet.instMin {α : Type u_1} [LE α] : Min (UpperSet α)

Equations

• UpperSet.instMin = { min := fun (s t : UpperSet α) => { carrier := ↑s ∪ ↑t, upper' := ⋯ } }

instance UpperSet.instTop {α : Type u_1} [LE α] : Top (UpperSet α)

Equations

• UpperSet.instTop = { top := { carrier := ∅, upper' := ⋯ } }

instance UpperSet.instBot {α : Type u_1} [LE α] : Bot (UpperSet α)

Equations

• UpperSet.instBot = { bot := { carrier := Set.univ, upper' := ⋯ } }

instance UpperSet.instSupSet {α : Type u_1} [LE α] : SupSet (UpperSet α)

Equations

• UpperSet.instSupSet = { sSup := fun (S : Set (UpperSet α)) => { carrier := ⋂ s ∈ S, ↑s, upper' := ⋯ } }

instance UpperSet.instInfSet {α : Type u_1} [LE α] : InfSet (UpperSet α)

Equations

• UpperSet.instInfSet = { sInf := fun (S : Set (UpperSet α)) => { carrier := ⋃ s ∈ S, ↑s, upper' := ⋯ } }

instance UpperSet.completeLattice {α : Type u_1} [LE α] : CompleteLattice (UpperSet α)

Equations

• UpperSet.completeLattice = Function.Injective.completeLattice (⇑OrderDual.toDual ∘ SetLike.coe) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance UpperSet.completelyDistribLattice {α : Type u_1} [LE α] : CompletelyDistribLattice (UpperSet α)

Equations

• One or more equations did not get rendered due to their size.

instance UpperSet.instInhabited {α : Type u_1} [LE α] : Inhabited (UpperSet α)

Equations

• UpperSet.instInhabited = { default := ⊥ }

@[simp]

theorem UpperSet.coe_subset_coe {α : Type u_1} [LE α] {s t : UpperSet α} : ↑s ⊆ ↑t ↔ t ≤ s

@[simp]

theorem UpperSet.coe_ssubset_coe {α : Type u_1} [LE α] {s t : UpperSet α} : ↑s ⊂ ↑t ↔ t < s

@[simp]

theorem UpperSet.coe_top {α : Type u_1} [LE α] : ↑⊤ = ∅

@[simp]

theorem UpperSet.coe_bot {α : Type u_1} [LE α] : ↑⊥ = Set.univ

@[simp]

theorem UpperSet.coe_eq_univ {α : Type u_1} [LE α] {s : UpperSet α} : ↑s = Set.univ ↔ s = ⊥

@[simp]

theorem UpperSet.coe_eq_empty {α : Type u_1} [LE α] {s : UpperSet α} : ↑s = ∅ ↔ s = ⊤

@[simp]

theorem UpperSet.coe_nonempty {α : Type u_1} [LE α] {s : UpperSet α} : (↑s).Nonempty ↔ s ≠ ⊤

@[simp]

theorem UpperSet.coe_sup {α : Type u_1} [LE α] (s t : UpperSet α) : ↑(s ⊔ t) = ↑s ∩ ↑t

@[simp]

theorem UpperSet.coe_inf {α : Type u_1} [LE α] (s t : UpperSet α) : ↑(s ⊓ t) = ↑s ∪ ↑t

@[simp]

theorem UpperSet.coe_sSup {α : Type u_1} [LE α] (S : Set (UpperSet α)) : ↑(sSup S) = ⋂ s ∈ S, ↑s

@[simp]

theorem UpperSet.coe_sInf {α : Type u_1} [LE α] (S : Set (UpperSet α)) : ↑(sInf S) = ⋃ s ∈ S, ↑s

@[simp]

theorem UpperSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) : ↑(⨆ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

@[simp]

theorem UpperSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) : ↑(⨅ (i : ι), f i) = ⋃ (i : ι), ↑(f i)

theorem UpperSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → UpperSet α) : ↑(⨆ (i : ι), ⨆ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), ↑(f i j)

theorem UpperSet.coe_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → UpperSet α) : ↑(⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋃ (i : ι), ⋃ (j : κ i), ↑(f i j)

@[simp]

theorem UpperSet.notMem_top {α : Type u_1} [LE α] {a : α} : a ∉ ⊤

@[deprecated UpperSet.notMem_top (since := "2025-05-23")]

theorem UpperSet.not_mem_top {α : Type u_1} [LE α] {a : α} : a ∉ ⊤

Alias of UpperSet.notMem_top.

@[simp]

theorem UpperSet.mem_bot {α : Type u_1} [LE α] {a : α} : a ∈ ⊥

@[simp]

theorem UpperSet.mem_sup_iff {α : Type u_1} [LE α] {s t : UpperSet α} {a : α} : a ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t

@[simp]

theorem UpperSet.mem_inf_iff {α : Type u_1} [LE α] {s t : UpperSet α} {a : α} : a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem UpperSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set (UpperSet α)} {a : α} : a ∈ sSup S ↔ ∀ s ∈ S, a ∈ s

@[simp]

theorem UpperSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (UpperSet α)} {a : α} : a ∈ sInf S ↔ ∃ s ∈ S, a ∈ s

@[simp]

theorem UpperSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → UpperSet α} : a ∈ ⨆ (i : ι), f i ↔ ∀ (i : ι), a ∈ f i

@[simp]

theorem UpperSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → UpperSet α} : a ∈ ⨅ (i : ι), f i ↔ ∃ (i : ι), a ∈ f i

theorem UpperSet.mem_iSup₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {a : α} {f : (i : ι) → κ i → UpperSet α} : a ∈ ⨆ (i : ι), ⨆ (j : κ i), f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

theorem UpperSet.mem_iInf₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {a : α} {f : (i : ι) → κ i → UpperSet α} : a ∈ ⨅ (i : ι), ⨅ (j : κ i), f i j ↔ ∃ (i : ι) (j : κ i), a ∈ f i j

@[simp]

theorem UpperSet.codisjoint_coe {α : Type u_1} [LE α] {s t : UpperSet α} : Codisjoint ↑s ↑t ↔ Disjoint s t

instance LowerSet.instMax {α : Type u_1} [LE α] : Max (LowerSet α)

Equations

• LowerSet.instMax = { max := fun (s t : LowerSet α) => { carrier := ↑s ∪ ↑t, lower' := ⋯ } }

instance LowerSet.instMin {α : Type u_1} [LE α] : Min (LowerSet α)

Equations

• LowerSet.instMin = { min := fun (s t : LowerSet α) => { carrier := ↑s ∩ ↑t, lower' := ⋯ } }

instance LowerSet.instTop {α : Type u_1} [LE α] : Top (LowerSet α)

Equations

• LowerSet.instTop = { top := { carrier := Set.univ, lower' := ⋯ } }

instance LowerSet.instBot {α : Type u_1} [LE α] : Bot (LowerSet α)

Equations

• LowerSet.instBot = { bot := { carrier := ∅, lower' := ⋯ } }

instance LowerSet.instSupSet {α : Type u_1} [LE α] : SupSet (LowerSet α)

Equations

• LowerSet.instSupSet = { sSup := fun (S : Set (LowerSet α)) => { carrier := ⋃ s ∈ S, ↑s, lower' := ⋯ } }

instance LowerSet.instInfSet {α : Type u_1} [LE α] : InfSet (LowerSet α)

Equations

• LowerSet.instInfSet = { sInf := fun (S : Set (LowerSet α)) => { carrier := ⋂ s ∈ S, ↑s, lower' := ⋯ } }

instance LowerSet.completeLattice {α : Type u_1} [LE α] : CompleteLattice (LowerSet α)

Equations

• LowerSet.completeLattice = Function.Injective.completeLattice SetLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance LowerSet.completelyDistribLattice {α : Type u_1} [LE α] : CompletelyDistribLattice (LowerSet α)

Equations

• One or more equations did not get rendered due to their size.

instance LowerSet.instInhabited {α : Type u_1} [LE α] : Inhabited (LowerSet α)

Equations

• LowerSet.instInhabited = { default := ⊥ }

theorem LowerSet.coe_subset_coe {α : Type u_1} [LE α] {s t : LowerSet α} : ↑s ⊆ ↑t ↔ s ≤ t

theorem LowerSet.coe_ssubset_coe {α : Type u_1} [LE α] {s t : LowerSet α} : ↑s ⊂ ↑t ↔ s < t

@[simp]

theorem LowerSet.coe_top {α : Type u_1} [LE α] : ↑⊤ = Set.univ

@[simp]

theorem LowerSet.coe_bot {α : Type u_1} [LE α] : ↑⊥ = ∅

@[simp]

theorem LowerSet.coe_eq_univ {α : Type u_1} [LE α] {s : LowerSet α} : ↑s = Set.univ ↔ s = ⊤

@[simp]

theorem LowerSet.coe_eq_empty {α : Type u_1} [LE α] {s : LowerSet α} : ↑s = ∅ ↔ s = ⊥

@[simp]

theorem LowerSet.coe_nonempty {α : Type u_1} [LE α] {s : LowerSet α} : (↑s).Nonempty ↔ s ≠ ⊥

@[simp]

theorem LowerSet.coe_sup {α : Type u_1} [LE α] (s t : LowerSet α) : ↑(s ⊔ t) = ↑s ∪ ↑t

@[simp]

theorem LowerSet.coe_inf {α : Type u_1} [LE α] (s t : LowerSet α) : ↑(s ⊓ t) = ↑s ∩ ↑t

@[simp]

theorem LowerSet.coe_sSup {α : Type u_1} [LE α] (S : Set (LowerSet α)) : ↑(sSup S) = ⋃ s ∈ S, ↑s

@[simp]

theorem LowerSet.coe_sInf {α : Type u_1} [LE α] (S : Set (LowerSet α)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem LowerSet.coe_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) : ↑(⨆ (i : ι), f i) = ⋃ (i : ι), ↑(f i)

@[simp]

theorem LowerSet.coe_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) : ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

theorem LowerSet.coe_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → LowerSet α) : ↑(⨆ (i : ι), ⨆ (j : κ i), f i j) = ⋃ (i : ι), ⋃ (j : κ i), ↑(f i j)

theorem LowerSet.coe_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → LowerSet α) : ↑(⨅ (i : ι), ⨅ (j : κ i), f i j) = ⋂ (i : ι), ⋂ (j : κ i), ↑(f i j)

@[simp]

theorem LowerSet.mem_top {α : Type u_1} [LE α] {a : α} : a ∈ ⊤

@[simp]

theorem LowerSet.notMem_bot {α : Type u_1} [LE α] {a : α} : a ∉ ⊥

@[deprecated LowerSet.notMem_bot (since := "2025-05-23")]

theorem LowerSet.not_mem_bot {α : Type u_1} [LE α] {a : α} : a ∉ ⊥

Alias of LowerSet.notMem_bot.

@[simp]

theorem LowerSet.mem_sup_iff {α : Type u_1} [LE α] {s t : LowerSet α} {a : α} : a ∈ s ⊔ t ↔ a ∈ s ∨ a ∈ t

@[simp]

theorem LowerSet.mem_inf_iff {α : Type u_1} [LE α] {s t : LowerSet α} {a : α} : a ∈ s ⊓ t ↔ a ∈ s ∧ a ∈ t

@[simp]

theorem LowerSet.mem_sSup_iff {α : Type u_1} [LE α] {S : Set (LowerSet α)} {a : α} : a ∈ sSup S ↔ ∃ s ∈ S, a ∈ s

@[simp]

theorem LowerSet.mem_sInf_iff {α : Type u_1} [LE α] {S : Set (LowerSet α)} {a : α} : a ∈ sInf S ↔ ∀ s ∈ S, a ∈ s

@[simp]

theorem LowerSet.mem_iSup_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → LowerSet α} : a ∈ ⨆ (i : ι), f i ↔ ∃ (i : ι), a ∈ f i

@[simp]

theorem LowerSet.mem_iInf_iff {α : Type u_1} {ι : Sort u_4} [LE α] {a : α} {f : ι → LowerSet α} : a ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), a ∈ f i

theorem LowerSet.mem_iSup₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {a : α} {f : (i : ι) → κ i → LowerSet α} : a ∈ ⨆ (i : ι), ⨆ (j : κ i), f i j ↔ ∃ (i : ι) (j : κ i), a ∈ f i j

theorem LowerSet.mem_iInf₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] {a : α} {f : (i : ι) → κ i → LowerSet α} : a ∈ ⨅ (i : ι), ⨅ (j : κ i), f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

@[simp]

theorem LowerSet.disjoint_coe {α : Type u_1} [LE α] {s t : LowerSet α} : Disjoint ↑s ↑t ↔ Disjoint s t

Complement

def UpperSet.compl {α : Type u_1} [LE α] (s : UpperSet α) : LowerSet α

The complement of a lower set as an upper set.

Equations

• s.compl = { carrier := (↑s)ᶜ, lower' := ⋯ }

def LowerSet.compl {α : Type u_1} [LE α] (s : LowerSet α) : UpperSet α

The complement of a lower set as an upper set.

Equations

• s.compl = { carrier := (↑s)ᶜ, upper' := ⋯ }

@[simp]

theorem UpperSet.coe_compl {α : Type u_1} [LE α] (s : UpperSet α) : ↑s.compl = (↑s)ᶜ

@[simp]

theorem UpperSet.mem_compl_iff {α : Type u_1} [LE α] {s : UpperSet α} {a : α} : a ∈ s.compl ↔ a ∉ s

@[simp]

theorem UpperSet.compl_compl {α : Type u_1} [LE α] (s : UpperSet α) : s.compl.compl = s

@[simp]

theorem UpperSet.compl_le_compl {α : Type u_1} [LE α] {s t : UpperSet α} : s.compl ≤ t.compl ↔ s ≤ t

@[simp]

theorem UpperSet.compl_sup {α : Type u_1} [LE α] (s t : UpperSet α) : (s ⊔ t).compl = s.compl ⊔ t.compl

@[simp]

theorem UpperSet.compl_inf {α : Type u_1} [LE α] (s t : UpperSet α) : (s ⊓ t).compl = s.compl ⊓ t.compl

@[simp]

theorem UpperSet.compl_top {α : Type u_1} [LE α] : ⊤.compl = ⊤

@[simp]

theorem UpperSet.compl_bot {α : Type u_1} [LE α] : ⊥.compl = ⊥

@[simp]

theorem UpperSet.compl_sSup {α : Type u_1} [LE α] (S : Set (UpperSet α)) : (sSup S).compl = ⨆ s ∈ S, s.compl

@[simp]

theorem UpperSet.compl_sInf {α : Type u_1} [LE α] (S : Set (UpperSet α)) : (sInf S).compl = ⨅ s ∈ S, s.compl

@[simp]

theorem UpperSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) : (⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl

@[simp]

theorem UpperSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → UpperSet α) : (⨅ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl

theorem UpperSet.compl_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → UpperSet α) : (⨆ (i : ι), ⨆ (j : κ i), f i j).compl = ⨆ (i : ι), ⨆ (j : κ i), (f i j).compl

theorem UpperSet.compl_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → UpperSet α) : (⨅ (i : ι), ⨅ (j : κ i), f i j).compl = ⨅ (i : ι), ⨅ (j : κ i), (f i j).compl

@[simp]

theorem LowerSet.coe_compl {α : Type u_1} [LE α] (s : LowerSet α) : ↑s.compl = (↑s)ᶜ

@[simp]

theorem LowerSet.mem_compl_iff {α : Type u_1} [LE α] {s : LowerSet α} {a : α} : a ∈ s.compl ↔ a ∉ s

@[simp]

theorem LowerSet.compl_compl {α : Type u_1} [LE α] (s : LowerSet α) : s.compl.compl = s

@[simp]

theorem LowerSet.compl_le_compl {α : Type u_1} [LE α] {s t : LowerSet α} : s.compl ≤ t.compl ↔ s ≤ t

theorem LowerSet.compl_sup {α : Type u_1} [LE α] (s t : LowerSet α) : (s ⊔ t).compl = s.compl ⊔ t.compl

theorem LowerSet.compl_inf {α : Type u_1} [LE α] (s t : LowerSet α) : (s ⊓ t).compl = s.compl ⊓ t.compl

theorem LowerSet.compl_top {α : Type u_1} [LE α] : ⊤.compl = ⊤

theorem LowerSet.compl_bot {α : Type u_1} [LE α] : ⊥.compl = ⊥

theorem LowerSet.compl_sSup {α : Type u_1} [LE α] (S : Set (LowerSet α)) : (sSup S).compl = ⨆ s ∈ S, s.compl

theorem LowerSet.compl_sInf {α : Type u_1} [LE α] (S : Set (LowerSet α)) : (sInf S).compl = ⨅ s ∈ S, s.compl

theorem LowerSet.compl_iSup {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) : (⨆ (i : ι), f i).compl = ⨆ (i : ι), (f i).compl

theorem LowerSet.compl_iInf {α : Type u_1} {ι : Sort u_4} [LE α] (f : ι → LowerSet α) : (⨅ (i : ι), f i).compl = ⨅ (i : ι), (f i).compl

@[simp]

theorem LowerSet.compl_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → LowerSet α) : (⨆ (i : ι), ⨆ (j : κ i), f i j).compl = ⨆ (i : ι), ⨆ (j : κ i), (f i j).compl

@[simp]

theorem LowerSet.compl_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [LE α] (f : (i : ι) → κ i → LowerSet α) : (⨅ (i : ι), ⨅ (j : κ i), f i j).compl = ⨅ (i : ι), ⨅ (j : κ i), (f i j).compl

def upperSetIsoLowerSet {α : Type u_1} [LE α] : UpperSet α ≃o LowerSet α

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

@[simp]

theorem upperSetIsoLowerSet_apply {α : Type u_1} [LE α] (s : UpperSet α) : upperSetIsoLowerSet s = s.compl

@[simp]

theorem upperSetIsoLowerSet_symm_apply {α : Type u_1} [LE α] (s : LowerSet α) : (RelIso.symm upperSetIsoLowerSet) s = s.compl

instance UpperSet.isTotal_le {α : Type u_1} [LinearOrder α] : IsTotal (UpperSet α) fun (x1 x2 : UpperSet α) => x1 ≤ x2

instance LowerSet.isTotal_le {α : Type u_1} [LinearOrder α] : IsTotal (LowerSet α) fun (x1 x2 : LowerSet α) => x1 ≤ x2

noncomputable instance UpperSet.instLinearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (UpperSet α)

Equations

• UpperSet.instLinearOrder = Lattice.toLinearOrder (UpperSet α)

noncomputable instance LowerSet.instLinearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (LowerSet α)

Equations

• LowerSet.instLinearOrder = Lattice.toLinearOrder (LowerSet α)

noncomputable instance UpperSet.instCompleteLinearOrder {α : Type u_1} [LinearOrder α] : CompleteLinearOrder (UpperSet α)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance LowerSet.instCompleteLinearOrder {α : Type u_1} [LinearOrder α] : CompleteLinearOrder (LowerSet α)

Equations

• One or more equations did not get rendered due to their size.

def UpperSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) : UpperSet α ≃o UpperSet β

An order isomorphism of Preorders induces an order isomorphism of their upper sets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem UpperSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α ≃o β} {s : UpperSet α} {b : β} : b ∈ (map f) s ↔ f.symm b ∈ s

@[simp]

theorem UpperSet.map_refl {α : Type u_1} [Preorder α] : map (OrderIso.refl α) = OrderIso.refl (UpperSet α)

@[simp]

theorem UpperSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : UpperSet α} (g : β ≃o γ) (f : α ≃o β) : (map g) ((map f) s) = (map (f.trans g)) s

@[simp]

theorem UpperSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) : ↑((map f) s) = ⇑f '' ↑s

def LowerSet.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) : LowerSet α ≃o LowerSet β

An order isomorphism of Preorders induces an order isomorphism of their lower sets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem LowerSet.mem_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : LowerSet α} {f : α ≃o β} {b : β} : b ∈ (map f) s ↔ f.symm b ∈ s

@[simp]

theorem LowerSet.map_refl {α : Type u_1} [Preorder α] : map (OrderIso.refl α) = OrderIso.refl (LowerSet α)

@[simp]

theorem LowerSet.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {s : LowerSet α} (g : β ≃o γ) (f : α ≃o β) : (map g) ((map f) s) = (map (f.trans g)) s

@[simp]

theorem LowerSet.coe_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) : ↑((map f) s) = ⇑f '' ↑s

@[simp]

theorem UpperSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : UpperSet α) : ((map f) s).compl = (LowerSet.map f) s.compl

@[simp]

theorem LowerSet.compl_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ≃o β) (s : LowerSet α) : ((map f) s).compl = (UpperSet.map f) s.compl