Documentation

Mathlib.Order.UpperLower.CompleteLattice

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

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

Set α

See Note [custom simps projection].

Equations

Instances For

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

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

Set α

See Note [custom simps projection].

Equations

Instances For

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

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

Min (UpperSet α)

Equations

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

Top (UpperSet α)

Equations

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

Bot (UpperSet α)

Equations

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

SupSet (UpperSet α)

Equations

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

InfSet (UpperSet α)

Equations

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

CompleteLattice (UpperSet α)

Equations

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

CompletelyDistribLattice (UpperSet α)

Equations

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

Inhabited (UpperSet α)

Equations

@[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 : α} :

@[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

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

Min (LowerSet α)

Equations

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

Top (LowerSet α)

Equations

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

Bot (LowerSet α)

Equations

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

SupSet (LowerSet α)

Equations

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

InfSet (LowerSet α)

Equations

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

CompleteLattice (LowerSet α)

Equations

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

CompletelyDistribLattice (LowerSet α)

Equations

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

Inhabited (LowerSet α)

Equations

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 : α} :

@[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 α) :

The complement of a lower set as an upper set.

Equations

Instances For

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

The complement of a lower set as an upper set.

Equations

Instances For

@[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

Instances For

@[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

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

LinearOrder (LowerSet α)

Equations

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

CompleteLinearOrder (UpperSet α)

Equations

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

CompleteLinearOrder (LowerSet α)

Equations

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

Instances For

@[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

Instances For

@[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