Sets closed under join/meet

This file defines predicates for sets closed under ⊔ and shows that each set in a join-semilattice generates a join-closed set and that a semilattice where every directed set has a least upper bound is automatically complete. All dually for ⊓.

Main declarations

• SupClosed: Predicate for a set to be closed under join (a ∈ s and b ∈ s imply a ⊔ b ∈ s).
• InfClosed: Predicate for a set to be closed under meet (a ∈ s and b ∈ s imply a ⊓ b ∈ s).
• supClosure: Sup-closure. Smallest sup-closed set containing a given set.
• infClosure: Inf-closure. Smallest inf-closed set containing a given set.
• SemilatticeSup.toCompleteSemilatticeSup: A join-semilattice where every sup-closed set has a least upper bound is automatically complete.
• SemilatticeInf.toCompleteSemilatticeInf: A meet-semilattice where every inf-closed set has a greatest lower bound is automatically complete.

def SupClosed {α : Type u_1} [SemilatticeSup α] (s : Set α) : Prop

A set s is sup-closed if a ⊔ b ∈ s for all a ∈ s, b ∈ s.

Equations

• SupClosed s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ⊔ b ∈ s

@[simp]

theorem supClosed_empty {α : Type u_1} [SemilatticeSup α] : SupClosed ∅

@[simp]

theorem supClosed_singleton {α : Type u_1} [SemilatticeSup α] {a : α} : SupClosed {a}

@[simp]

theorem supClosed_univ {α : Type u_1} [SemilatticeSup α] : SupClosed Set.univ

theorem SupClosed.inter {α : Type u_1} [SemilatticeSup α] {s : Set α} {t : Set α} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ∩ t)

theorem supClosed_sInter {α : Type u_1} [SemilatticeSup α] {S : Set (Set α)} (hS : ∀ (s : Set α), s ∈ S → SupClosed s) : SupClosed (⋂₀ S)

theorem supClosed_iInter {α : Type u_1} [SemilatticeSup α] {ι : Sort u_2} {f : ι → Set α} (hf : ∀ (i : ι), SupClosed (f i)) : SupClosed (⋂ (i : ι), f i)

theorem SupClosed.directedOn {α : Type u_1} [SemilatticeSup α] {s : Set α} (hs : SupClosed s) : DirectedOn (fun x x_1 => x ≤ x_1) s

theorem IsUpperSet.supClosed {α : Type u_1} [SemilatticeSup α] {s : Set α} (hs : IsUpperSet s) : SupClosed s

theorem SupClosed.finsetSup'_mem {α : Type u_1} [SemilatticeSup α] {ι : Type u_2} {f : ι → α} {s : Set α} {t : Finset ι} (hs : SupClosed s) (ht : Finset.Nonempty t) : (∀ (i : ι), i ∈ t → f i ∈ s) → Finset.sup' t ht f ∈ s

theorem SupClosed.finsetSup_mem {α : Type u_1} [SemilatticeSup α] {ι : Type u_2} {f : ι → α} {s : Set α} {t : Finset ι} [OrderBot α] (hs : SupClosed s) (ht : Finset.Nonempty t) : (∀ (i : ι), i ∈ t → f i ∈ s) → Finset.sup t f ∈ s

def InfClosed {α : Type u_1} [SemilatticeInf α] (s : Set α) : Prop

A set s is inf-closed if a ⊓ b ∈ s for all a ∈ s, b ∈ s.

Equations

• InfClosed s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ⊓ b ∈ s

@[simp]

theorem infClosed_empty {α : Type u_1} [SemilatticeInf α] : InfClosed ∅

@[simp]

theorem infClosed_singleton {α : Type u_1} [SemilatticeInf α] {a : α} : InfClosed {a}

@[simp]

theorem infClosed_univ {α : Type u_1} [SemilatticeInf α] : InfClosed Set.univ

theorem InfClosed.inter {α : Type u_1} [SemilatticeInf α] {s : Set α} {t : Set α} (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ∩ t)

theorem infClosed_sInter {α : Type u_1} [SemilatticeInf α] {S : Set (Set α)} (hS : ∀ (s : Set α), s ∈ S → InfClosed s) : InfClosed (⋂₀ S)

theorem infClosed_iInter {α : Type u_1} [SemilatticeInf α] {ι : Sort u_2} {f : ι → Set α} (hf : ∀ (i : ι), InfClosed (f i)) : InfClosed (⋂ (i : ι), f i)

theorem InfClosed.codirectedOn {α : Type u_1} [SemilatticeInf α] {s : Set α} (hs : InfClosed s) : DirectedOn (fun x x_1 => x ≥ x_1) s

theorem IsLowerSet.infClosed {α : Type u_1} [SemilatticeInf α] {s : Set α} (hs : IsLowerSet s) : InfClosed s

theorem InfClosed.finsetInf'_mem {α : Type u_1} [SemilatticeInf α] {ι : Type u_2} {f : ι → α} {s : Set α} {t : Finset ι} (hs : InfClosed s) (ht : Finset.Nonempty t) : (∀ (i : ι), i ∈ t → f i ∈ s) → Finset.inf' t ht f ∈ s

theorem InfClosed.finsetInf_mem {α : Type u_1} [SemilatticeInf α] {ι : Type u_2} {f : ι → α} {s : Set α} {t : Finset ι} [OrderTop α] (hs : InfClosed s) (ht : Finset.Nonempty t) : (∀ (i : ι), i ∈ t → f i ∈ s) → Finset.inf t f ∈ s

@[simp]

theorem supClosed_preimage_toDual {α : Type u_1} [Lattice α] {s : Set αᵒᵈ} : SupClosed (↑OrderDual.toDual ⁻¹' s) ↔ InfClosed s

@[simp]

theorem infClosed_preimage_toDual {α : Type u_1} [Lattice α] {s : Set αᵒᵈ} : InfClosed (↑OrderDual.toDual ⁻¹' s) ↔ SupClosed s

@[simp]

theorem supClosed_preimage_ofDual {α : Type u_1} [Lattice α] {s : Set α} : SupClosed (↑OrderDual.ofDual ⁻¹' s) ↔ InfClosed s

@[simp]

theorem infClosed_preimage_ofDual {α : Type u_1} [Lattice α] {s : Set α} : InfClosed (↑OrderDual.ofDual ⁻¹' s) ↔ SupClosed s

theorem InfClosed.dual {α : Type u_1} [Lattice α] {s : Set α} : InfClosed s → SupClosed (↑OrderDual.ofDual ⁻¹' s)

Alias of the reverse direction of supClosed_preimage_ofDual.

theorem SupClosed.dual {α : Type u_1} [Lattice α] {s : Set α} : SupClosed s → InfClosed (↑OrderDual.ofDual ⁻¹' s)

Alias of the reverse direction of infClosed_preimage_ofDual.

@[simp]

theorem LinearOrder.supClosed {α : Type u_1} [LinearOrder α] (s : Set α) : SupClosed s

@[simp]

theorem LinearOrder.infClosed {α : Type u_1} [LinearOrder α] (s : Set α) : InfClosed s

Closure

def supClosure {α : Type u_1} [SemilatticeSup α] : ClosureOperator (Set α)

Every set in a join-semilattice generates a set closed under join.

Equations

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

@[simp]

theorem subset_supClosure {α : Type u_1} [SemilatticeSup α] {s : Set α} : s ⊆ ↑supClosure s

@[simp]

theorem supClosed_supClosure {α : Type u_1} [SemilatticeSup α] {s : Set α} : SupClosed (↑supClosure s)

theorem supClosure_mono {α : Type u_1} [SemilatticeSup α] : Monotone ↑supClosure

@[simp]

theorem supClosure_eq_self {α : Type u_1} [SemilatticeSup α] {s : Set α} : ↑supClosure s = s ↔ SupClosed s

theorem SupClosed.supClosure_eq {α : Type u_1} [SemilatticeSup α] {s : Set α} : SupClosed s → ↑supClosure s = s

Alias of the reverse direction of supClosure_eq_self.

theorem supClosure_idem {α : Type u_1} [SemilatticeSup α] (s : Set α) : ↑supClosure (↑supClosure s) = ↑supClosure s

@[simp]

theorem supClosure_empty {α : Type u_1} [SemilatticeSup α] : ↑supClosure ∅ = ∅

@[simp]

theorem supClosure_singleton {α : Type u_1} [SemilatticeSup α] {a : α} : ↑supClosure {a} = {a}

@[simp]

theorem supClosure_univ {α : Type u_1} [SemilatticeSup α] : ↑supClosure Set.univ = Set.univ

@[simp]

theorem upperBounds_supClosure {α : Type u_1} [SemilatticeSup α] (s : Set α) : upperBounds (↑supClosure s) = upperBounds s

@[simp]

theorem isLUB_supClosure {α : Type u_1} [SemilatticeSup α] {s : Set α} {a : α} : IsLUB (↑supClosure s) a ↔ IsLUB s a

def infClosure {α : Type u_1} [SemilatticeInf α] : ClosureOperator (Set α)

Every set in a join-semilattice generates a set closed under join.

Equations

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

@[simp]

theorem subset_infClosure {α : Type u_1} [SemilatticeInf α] {s : Set α} : s ⊆ ↑infClosure s

@[simp]

theorem infClosed_infClosure {α : Type u_1} [SemilatticeInf α] {s : Set α} : InfClosed (↑infClosure s)

theorem infClosure_mono {α : Type u_1} [SemilatticeInf α] : Monotone ↑infClosure

@[simp]

theorem infClosure_eq_self {α : Type u_1} [SemilatticeInf α] {s : Set α} : ↑infClosure s = s ↔ InfClosed s

theorem InfClosed.infClosure_eq {α : Type u_1} [SemilatticeInf α] {s : Set α} : InfClosed s → ↑infClosure s = s

Alias of the reverse direction of infClosure_eq_self.

theorem infClosure_idem {α : Type u_1} [SemilatticeInf α] (s : Set α) : ↑infClosure (↑infClosure s) = ↑infClosure s

@[simp]

theorem infClosure_empty {α : Type u_1} [SemilatticeInf α] : ↑infClosure ∅ = ∅

@[simp]

theorem infClosure_singleton {α : Type u_1} [SemilatticeInf α] {a : α} : ↑infClosure {a} = {a}

@[simp]

theorem infClosure_univ {α : Type u_1} [SemilatticeInf α] : ↑infClosure Set.univ = Set.univ

@[simp]

theorem lowerBounds_infClosure {α : Type u_1} [SemilatticeInf α] (s : Set α) : lowerBounds (↑infClosure s) = lowerBounds s

@[simp]

theorem isGLB_infClosure {α : Type u_1} [SemilatticeInf α] {s : Set α} {a : α} : IsGLB (↑infClosure s) a ↔ IsGLB s a

def SemilatticeSup.toCompleteSemilatticeSup {α : Type u_1} [SemilatticeSup α] (sSup : Set α → α) (h : ∀ (s : Set α), SupClosed s → IsLUB s (sSup s)) : CompleteSemilatticeSup α

A join-semilattice where every sup-closed set has a least upper bound is automatically complete.

Equations

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

def SemilatticeInf.toCompleteSemilatticeInf {α : Type u_1} [SemilatticeInf α] (sInf : Set α → α) (h : ∀ (s : Set α), InfClosed s → IsGLB s (sInf s)) : CompleteSemilatticeInf α

A meet-semilattice where every inf-closed set has a greatest lower bound is automatically complete.

Equations

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