Upper and lower closures

Upper (lower) closures generalise principal upper (lower) sets to arbitrary included sets. Indeed, they are equivalent to a union over principal upper (lower) sets, as shown in coe_upperClosure (coe_lowerClosure).

Main declarations

• upperClosure: The greatest upper set containing a set.
• lowerClosure: The least lower set containing a set.

def upperClosure {α : Type u_1} [Preorder α] (s : Set α) : UpperSet α

The greatest upper set containing a given set.

Equations

• upperClosure s = { carrier := {x : α | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }

def lowerClosure {α : Type u_1} [Preorder α] (s : Set α) : LowerSet α

The least lower set containing a given set.

Equations

• lowerClosure s = { carrier := {x : α | ∃ a ∈ s, x ≤ a}, lower' := ⋯ }

@[simp]

theorem mem_upperClosure {α : Type u_1} [Preorder α] {s : Set α} {x : α} : x ∈ upperClosure s ↔ ∃ a ∈ s, a ≤ x

@[simp]

theorem mem_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} {x : α} : x ∈ lowerClosure s ↔ ∃ a ∈ s, x ≤ a

theorem coe_upperClosure {α : Type u_1} [Preorder α] (s : Set α) : ↑(upperClosure s) = ⋃ a ∈ s, Set.Ici a

theorem coe_lowerClosure {α : Type u_1} [Preorder α] (s : Set α) : ↑(lowerClosure s) = ⋃ a ∈ s, Set.Iic a

instance instDecidablePredMemUpperClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun (x : α) => ∃ a ∈ s, a ≤ x] : DecidablePred fun (x : α) => x ∈ upperClosure s

Equations

• instDecidablePredMemUpperClosure = inst✝

instance instDecidablePredMemLowerClosure {α : Type u_1} [Preorder α] {s : Set α} [DecidablePred fun (x : α) => ∃ a ∈ s, x ≤ a] : DecidablePred fun (x : α) => x ∈ lowerClosure s

Equations

• instDecidablePredMemLowerClosure = inst✝

theorem subset_upperClosure {α : Type u_1} [Preorder α] {s : Set α} : s ⊆ ↑(upperClosure s)

theorem subset_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : s ⊆ ↑(lowerClosure s)

theorem upperClosure_min {α : Type u_1} [Preorder α] {s t : Set α} (h : s ⊆ t) (ht : IsUpperSet t) : ↑(upperClosure s) ⊆ t

theorem lowerClosure_min {α : Type u_1} [Preorder α] {s t : Set α} (h : s ⊆ t) (ht : IsLowerSet t) : ↑(lowerClosure s) ⊆ t

theorem IsUpperSet.upperClosure {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) : ↑(upperClosure s) = s

theorem IsLowerSet.lowerClosure {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) : ↑(lowerClosure s) = s

@[simp]

theorem UpperSet.upperClosure {α : Type u_1} [Preorder α] (s : UpperSet α) : upperClosure ↑s = s

@[simp]

theorem LowerSet.lowerClosure {α : Type u_1} [Preorder α] (s : LowerSet α) : lowerClosure ↑s = s

@[simp]

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

@[simp]

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

@[simp]

theorem UpperSet.iInf_Ici {α : Type u_1} [Preorder α] (s : Set α) : ⨅ a ∈ s, Ici a = upperClosure s

@[simp]

theorem LowerSet.iSup_Iic {α : Type u_1} [Preorder α] (s : Set α) : ⨆ a ∈ s, Iic a = lowerClosure s

@[simp]

theorem lowerClosure_le {α : Type u_1} [Preorder α] {s : Set α} {t : LowerSet α} : lowerClosure s ≤ t ↔ s ⊆ ↑t

@[simp]

theorem le_upperClosure {α : Type u_1} [Preorder α] {t : Set α} {s : UpperSet α} : s ≤ upperClosure t ↔ t ⊆ ↑s

theorem gc_upperClosure_coe {α : Type u_1} [Preorder α] : GaloisConnection (⇑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ⇑OrderDual.ofDual)

theorem gc_lowerClosure_coe {α : Type u_1} [Preorder α] : GaloisConnection lowerClosure SetLike.coe

def giUpperClosureCoe {α : Type u_1} [Preorder α] : GaloisInsertion (⇑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ⇑OrderDual.ofDual)

upperClosure forms a reversed Galois insertion with the coercion from upper sets to sets.

Equations

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

def giLowerClosureCoe {α : Type u_1} [Preorder α] : GaloisInsertion lowerClosure SetLike.coe

lowerClosure forms a Galois insertion with the coercion from lower sets to sets.

Equations

• giLowerClosureCoe = { choice := fun (s : Set α) (hs : ↑(lowerClosure s) ≤ s) => { carrier := s, lower' := ⋯ }, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

theorem upperClosure_anti {α : Type u_1} [Preorder α] : Antitone upperClosure

theorem lowerClosure_mono {α : Type u_1} [Preorder α] : Monotone lowerClosure

@[simp]

theorem upperClosure_empty {α : Type u_1} [Preorder α] : upperClosure ∅ = ⊤

@[simp]

theorem lowerClosure_empty {α : Type u_1} [Preorder α] : lowerClosure ∅ = ⊥

@[simp]

theorem upperClosure_singleton {α : Type u_1} [Preorder α] (a : α) : upperClosure {a} = UpperSet.Ici a

@[simp]

theorem lowerClosure_singleton {α : Type u_1} [Preorder α] (a : α) : lowerClosure {a} = LowerSet.Iic a

@[simp]

theorem upperClosure_univ {α : Type u_1} [Preorder α] : upperClosure Set.univ = ⊥

@[simp]

theorem lowerClosure_univ {α : Type u_1} [Preorder α] : lowerClosure Set.univ = ⊤

@[simp]

theorem upperClosure_eq_top_iff {α : Type u_1} [Preorder α] {s : Set α} : upperClosure s = ⊤ ↔ s = ∅

@[simp]

theorem lowerClosure_eq_bot_iff {α : Type u_1} [Preorder α] {s : Set α} : lowerClosure s = ⊥ ↔ s = ∅

@[simp]

theorem upperClosure_union {α : Type u_1} [Preorder α] (s t : Set α) : upperClosure (s ∪ t) = upperClosure s ⊓ upperClosure t

@[simp]

theorem lowerClosure_union {α : Type u_1} [Preorder α] (s t : Set α) : lowerClosure (s ∪ t) = lowerClosure s ⊔ lowerClosure t

@[simp]

theorem upperClosure_iUnion {α : Type u_1} {ι : Sort u_3} [Preorder α] (f : ι → Set α) : upperClosure (⋃ (i : ι), f i) = ⨅ (i : ι), upperClosure (f i)

@[simp]

theorem lowerClosure_iUnion {α : Type u_1} {ι : Sort u_3} [Preorder α] (f : ι → Set α) : lowerClosure (⋃ (i : ι), f i) = ⨆ (i : ι), lowerClosure (f i)

@[simp]

theorem upperClosure_sUnion {α : Type u_1} [Preorder α] (S : Set (Set α)) : upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s

@[simp]

theorem lowerClosure_sUnion {α : Type u_1} [Preorder α] (S : Set (Set α)) : lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s

theorem Set.OrdConnected.upperClosure_inter_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} (h : s.OrdConnected) : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

theorem ordConnected_iff_upperClosure_inter_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

@[simp]

theorem upperBounds_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : upperBounds ↑(lowerClosure s) = upperBounds s

@[simp]

theorem lowerBounds_upperClosure {α : Type u_1} [Preorder α] {s : Set α} : lowerBounds ↑(upperClosure s) = lowerBounds s

@[simp]

theorem bddAbove_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : BddAbove ↑(lowerClosure s) ↔ BddAbove s

@[simp]

theorem bddBelow_upperClosure {α : Type u_1} [Preorder α] {s : Set α} : BddBelow ↑(upperClosure s) ↔ BddBelow s

theorem BddAbove.lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : BddAbove s → BddAbove ↑(lowerClosure s)

Alias of the reverse direction of bddAbove_lowerClosure.

theorem BddAbove.of_lowerClosure {α : Type u_1} [Preorder α] {s : Set α} : BddAbove ↑(lowerClosure s) → BddAbove s

Alias of the forward direction of bddAbove_lowerClosure.

theorem BddBelow.of_upperClosure {α : Type u_1} [Preorder α] {s : Set α} : BddBelow ↑(upperClosure s) → BddBelow s

Alias of the forward direction of bddBelow_upperClosure.

theorem BddBelow.upperClosure {α : Type u_1} [Preorder α] {s : Set α} : BddBelow s → BddBelow ↑(upperClosure s)

Alias of the reverse direction of bddBelow_upperClosure.

@[simp]

theorem IsLowerSet.disjoint_upperClosure_left {α : Type u_1} [Preorder α] {s t : Set α} (ht : IsLowerSet t) : Disjoint (↑(upperClosure s)) t ↔ Disjoint s t

@[simp]

theorem IsLowerSet.disjoint_upperClosure_right {α : Type u_1} [Preorder α] {s t : Set α} (hs : IsLowerSet s) : Disjoint s ↑(upperClosure t) ↔ Disjoint s t

@[simp]

theorem IsUpperSet.disjoint_lowerClosure_left {α : Type u_1} [Preorder α] {s t : Set α} (ht : IsUpperSet t) : Disjoint (↑(lowerClosure s)) t ↔ Disjoint s t

@[simp]

theorem IsUpperSet.disjoint_lowerClosure_right {α : Type u_1} [Preorder α] {s t : Set α} (hs : IsUpperSet s) : Disjoint s ↑(lowerClosure t) ↔ Disjoint s t

@[simp]

theorem upperClosure_eq {α : Type u_1} [Preorder α] {s : Set α} : ↑(upperClosure s) = s ↔ IsUpperSet s

@[simp]

theorem lowerClosure_eq {α : Type u_1} [Preorder α] {s : Set α} : ↑(lowerClosure s) = s ↔ IsLowerSet s

Set Difference

def LowerSet.sdiff {α : Type u_1} [Preorder α] (s : LowerSet α) (t : Set α) : LowerSet α

The biggest lower subset of a lower set s disjoint from a set t.

Equations

• s.sdiff t = { carrier := ↑s \ ↑(upperClosure t), lower' := ⋯ }

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

The biggest lower subset of a lower set s not containing an element a.

Equations

• s.erase a = { carrier := ↑s \ ↑(UpperSet.Ici a), lower' := ⋯ }

@[simp]

theorem LowerSet.coe_sdiff {α : Type u_1} [Preorder α] (s : LowerSet α) (t : Set α) : ↑(s.sdiff t) = ↑s \ ↑(upperClosure t)

@[simp]

theorem LowerSet.coe_erase {α : Type u_1} [Preorder α] (s : LowerSet α) (a : α) : ↑(s.erase a) = ↑s \ ↑(UpperSet.Ici a)

@[simp]

theorem LowerSet.sdiff_singleton {α : Type u_1} [Preorder α] (s : LowerSet α) (a : α) : s.sdiff {a} = s.erase a

theorem LowerSet.sdiff_le_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} : s.sdiff t ≤ s

theorem LowerSet.erase_le {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} : s.erase a ≤ s

@[simp]

theorem LowerSet.sdiff_eq_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} : s.sdiff t = s ↔ Disjoint (↑s) t

@[simp]

theorem LowerSet.erase_eq {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} : s.erase a = s ↔ a ∉ s

@[simp]

theorem LowerSet.sdiff_lt_left {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} : s.sdiff t < s ↔ ¬Disjoint (↑s) t

@[simp]

theorem LowerSet.erase_lt {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} : s.erase a < s ↔ a ∈ s

@[simp]

theorem LowerSet.sdiff_idem {α : Type u_1} [Preorder α] (s : LowerSet α) (t : Set α) : (s.sdiff t).sdiff t = s.sdiff t

@[simp]

theorem LowerSet.erase_idem {α : Type u_1} [Preorder α] (s : LowerSet α) (a : α) : (s.erase a).erase a = s.erase a

theorem LowerSet.sdiff_sup_lowerClosure {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) : s.sdiff t ⊔ lowerClosure t = s

theorem LowerSet.lowerClosure_sup_sdiff {α : Type u_1} [Preorder α] {s : LowerSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) : lowerClosure t ⊔ s.sdiff t = s

theorem LowerSet.erase_sup_Iic {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : s.erase a ⊔ Iic a = s

theorem LowerSet.Iic_sup_erase {α : Type u_1} [Preorder α] {s : LowerSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, a ≤ b → b = a) : Iic a ⊔ s.erase a = s

def UpperSet.sdiff {α : Type u_1} [Preorder α] (s : UpperSet α) (t : Set α) : UpperSet α

The biggest upper subset of a upper set s disjoint from a set t.

Equations

• s.sdiff t = { carrier := ↑s \ ↑(lowerClosure t), upper' := ⋯ }

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

The biggest upper subset of a upper set s not containing an element a.

Equations

• s.erase a = { carrier := ↑s \ ↑(LowerSet.Iic a), upper' := ⋯ }

@[simp]

theorem UpperSet.coe_sdiff {α : Type u_1} [Preorder α] (s : UpperSet α) (t : Set α) : ↑(s.sdiff t) = ↑s \ ↑(lowerClosure t)

@[simp]

theorem UpperSet.coe_erase {α : Type u_1} [Preorder α] (s : UpperSet α) (a : α) : ↑(s.erase a) = ↑s \ ↑(LowerSet.Iic a)

@[simp]

theorem UpperSet.sdiff_singleton {α : Type u_1} [Preorder α] (s : UpperSet α) (a : α) : s.sdiff {a} = s.erase a

theorem UpperSet.le_sdiff_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} : s ≤ s.sdiff t

theorem UpperSet.le_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} : s ≤ s.erase a

@[simp]

theorem UpperSet.sdiff_eq_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} : s.sdiff t = s ↔ Disjoint (↑s) t

@[simp]

theorem UpperSet.erase_eq {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} : s.erase a = s ↔ a ∉ s

@[simp]

theorem UpperSet.lt_sdiff_left {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} : s < s.sdiff t ↔ ¬Disjoint (↑s) t

@[simp]

theorem UpperSet.lt_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} : s < s.erase a ↔ a ∈ s

@[simp]

theorem UpperSet.sdiff_idem {α : Type u_1} [Preorder α] (s : UpperSet α) (t : Set α) : (s.sdiff t).sdiff t = s.sdiff t

@[simp]

theorem UpperSet.erase_idem {α : Type u_1} [Preorder α] (s : UpperSet α) (a : α) : (s.erase a).erase a = s.erase a

theorem UpperSet.sdiff_inf_upperClosure {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) : s.sdiff t ⊓ upperClosure t = s

theorem UpperSet.upperClosure_inf_sdiff {α : Type u_1} [Preorder α] {s : UpperSet α} {t : Set α} (hts : t ⊆ ↑s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) : upperClosure t ⊓ s.sdiff t = s

theorem UpperSet.erase_inf_Ici {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : s.erase a ⊓ Ici a = s

theorem UpperSet.Ici_inf_erase {α : Type u_1} [Preorder α] {s : UpperSet α} {a : α} (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : Ici a ⊓ s.erase a = s