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).
• IsSublattice: Predicate for a set to be closed under meet and join.
• supClosure: Sup-closure. Smallest sup-closed set containing a given set.
• infClosure: Inf-closure. Smallest inf-closed set containing a given set.
• latticeClosure: Smallest sublattice 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_2} [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_2} [SemilatticeSup α] : SupClosed ∅

@[simp]

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

@[simp]

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

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

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

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

theorem SupClosed.directedOn {α : Type u_2} [SemilatticeSup α] {s : Set α} (hs : SupClosed s) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s

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

theorem SupClosed.preimage {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] {s : Set α} [FunLike F β α] [SupHomClass F β α] (hs : SupClosed s) (f : F) : SupClosed (⇑f ⁻¹' s)

theorem SupClosed.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] {s : Set α} [FunLike F α β] [SupHomClass F α β] (hs : SupClosed s) (f : F) : SupClosed (⇑f '' s)

theorem supClosed_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) : SupClosed (Set.range ⇑f)

theorem SupClosed.prod {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] {s : Set α} {t : Set β} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ×ˢ t)

theorem supClosed_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → SemilatticeSup (α i)] {s : Set ι} {t : (i : ι) → Set (α i)} (ht : ∀ i ∈ s, SupClosed (t i)) : SupClosed (s.pi t)

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

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

def InfClosed {α : Type u_2} [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_2} [SemilatticeInf α] : InfClosed ∅

@[simp]

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

@[simp]

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

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

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

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

theorem InfClosed.codirectedOn {α : Type u_2} [SemilatticeInf α] {s : Set α} (hs : InfClosed s) : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s

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

theorem InfClosed.preimage {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] {s : Set α} [FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) : InfClosed (⇑f ⁻¹' s)

theorem InfClosed.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] {s : Set α} [FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) : InfClosed (⇑f '' s)

theorem infClosed_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) : InfClosed (Set.range ⇑f)

theorem InfClosed.prod {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] {s : Set α} {t : Set β} (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ×ˢ t)

theorem infClosed_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → SemilatticeInf (α i)] {s : Set ι} {t : (i : ι) → Set (α i)} (ht : ∀ i ∈ s, InfClosed (t i)) : InfClosed (s.pi t)

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

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

structure IsSublattice {α : Type u_2} [Lattice α] (s : Set α) : Prop

A set s is a sublattice if a ⊔ b ∈ s and a ⊓ b ∈ s for all a ∈ s, b ∈ s. Note: This is not the preferred way to declare a sublattice. One should instead use Sublattice. TODO: Define Sublattice.

• supClosed : SupClosed s
• infClosed : InfClosed s

@[simp]

theorem isSublattice_empty {α : Type u_2} [Lattice α] : IsSublattice ∅

@[simp]

theorem isSublattice_singleton {α : Type u_2} [Lattice α] {a : α} : IsSublattice {a}

@[simp]

theorem isSublattice_univ {α : Type u_2} [Lattice α] : IsSublattice Set.univ

theorem IsSublattice.inter {α : Type u_2} [Lattice α] {s t : Set α} (hs : IsSublattice s) (ht : IsSublattice t) : IsSublattice (s ∩ t)

theorem isSublattice_sInter {α : Type u_2} [Lattice α] {S : Set (Set α)} (hS : ∀ s ∈ S, IsSublattice s) : IsSublattice (⋂₀ S)

theorem isSublattice_iInter {α : Type u_2} {ι : Sort u_4} [Lattice α] {f : ι → Set α} (hf : ∀ (i : ι), IsSublattice (f i)) : IsSublattice (⋂ (i : ι), f i)

theorem IsSublattice.preimage {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {s : Set α} [FunLike F β α] [LatticeHomClass F β α] (hs : IsSublattice s) (f : F) : IsSublattice (⇑f ⁻¹' s)

theorem IsSublattice.image {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {s : Set α} [FunLike F α β] [LatticeHomClass F α β] (hs : IsSublattice s) (f : F) : IsSublattice (⇑f '' s)

theorem IsSublattice_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [FunLike F α β] [LatticeHomClass F α β] (f : F) : IsSublattice (Set.range ⇑f)

theorem IsSublattice.prod {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {s : Set α} {t : Set β} (hs : IsSublattice s) (ht : IsSublattice t) : IsSublattice (s ×ˢ t)

theorem isSublattice_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Lattice (α i)] {s : Set ι} {t : (i : ι) → Set (α i)} (ht : ∀ i ∈ s, IsSublattice (t i)) : IsSublattice (s.pi t)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem isSublattice_preimage_toDual {α : Type u_2} [Lattice α] {s : Set αᵒᵈ} : IsSublattice (⇑OrderDual.toDual ⁻¹' s) ↔ IsSublattice s

@[simp]

theorem isSublattice_preimage_ofDual {α : Type u_2} [Lattice α] {s : Set α} : IsSublattice (⇑OrderDual.ofDual ⁻¹' s) ↔ IsSublattice s

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

Alias of the reverse direction of supClosed_preimage_ofDual.

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

Alias of the reverse direction of infClosed_preimage_ofDual.

theorem IsSublattice.dual {α : Type u_2} [Lattice α] {s : Set α} : IsSublattice s → IsSublattice (⇑OrderDual.ofDual ⁻¹' s)

Alias of the reverse direction of isSublattice_preimage_ofDual.

theorem IsSublattice.of_dual {α : Type u_2} [Lattice α] {s : Set αᵒᵈ} : IsSublattice s → IsSublattice (⇑OrderDual.toDual ⁻¹' s)

Alias of the reverse direction of isSublattice_preimage_toDual.

@[simp]

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

@[simp]

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

@[simp]

theorem LinearOrder.isSublattice {α : Type u_2} [LinearOrder α] (s : Set α) : IsSublattice s

Closure

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

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

Equations

• supClosure = ClosureOperator.ofPred (fun (s : Set α) => {a : α | ∃ (t : Finset α) (ht : t.Nonempty), ↑t ⊆ s ∧ t.sup' ht id = a}) SupClosed ⋯ ⋯ ⋯

@[simp]

theorem supClosure_isClosed {α : Type u_2} [SemilatticeSup α] (s : Set α) : supClosure.IsClosed s = SupClosed s

@[simp]

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

@[simp]

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

theorem supClosure_mono {α : Type u_2} [SemilatticeSup α] : Monotone ⇑supClosure

@[simp]

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

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

Alias of the reverse direction of supClosure_eq_self.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem sup_mem_supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} {a b : α} (ha : a ∈ s) (hb : b ∈ s) : a ⊔ b ∈ supClosure s

theorem finsetSup'_mem_supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} {ι : Type u_4} {t : Finset ι} (ht : t.Nonempty) {f : ι → α} (hf : ∀ i ∈ t, f i ∈ s) : t.sup' ht f ∈ supClosure s

theorem supClosure_min {α : Type u_2} [SemilatticeSup α] {s t : Set α} : s ⊆ t → SupClosed t → supClosure s ⊆ t

theorem Set.Finite.supClosure {α : Type u_2} [SemilatticeSup α] {s : Set α} (hs : s.Finite) : (supClosure s).Finite

The semilatice generated by a finite set is finite.

@[simp]

theorem supClosure_prod {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [SemilatticeSup β] (s : Set α) (t : Set β) : supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t

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

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

Equations

• infClosure = ClosureOperator.ofPred (fun (s : Set α) => {a : α | ∃ (t : Finset α) (ht : t.Nonempty), ↑t ⊆ s ∧ t.inf' ht id = a}) InfClosed ⋯ ⋯ ⋯

@[simp]

theorem infClosure_isClosed {α : Type u_2} [SemilatticeInf α] (s : Set α) : infClosure.IsClosed s = InfClosed s

@[simp]

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

@[simp]

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

theorem infClosure_mono {α : Type u_2} [SemilatticeInf α] : Monotone ⇑infClosure

@[simp]

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

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

Alias of the reverse direction of infClosure_eq_self.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem inf_mem_infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} {a b : α} (ha : a ∈ s) (hb : b ∈ s) : a ⊓ b ∈ infClosure s

theorem finsetInf'_mem_infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} {ι : Type u_4} {t : Finset ι} (ht : t.Nonempty) {f : ι → α} (hf : ∀ i ∈ t, f i ∈ s) : t.inf' ht f ∈ infClosure s

theorem infClosure_min {α : Type u_2} [SemilatticeInf α] {s t : Set α} : s ⊆ t → InfClosed t → infClosure s ⊆ t

theorem Set.Finite.infClosure {α : Type u_2} [SemilatticeInf α] {s : Set α} (hs : s.Finite) : (infClosure s).Finite

The semilatice generated by a finite set is finite.

@[simp]

theorem infClosure_prod {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [SemilatticeInf β] (s : Set α) (t : Set β) : infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t

def latticeClosure {α : Type u_2} [Lattice α] : ClosureOperator (Set α)

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

Equations

• latticeClosure = ClosureOperator.ofCompletePred IsSublattice ⋯

@[simp]

theorem latticeClosure_isClosed {α : Type u_2} [Lattice α] (s : Set α) : latticeClosure.IsClosed s = IsSublattice s

@[simp]

theorem subset_latticeClosure {α : Type u_2} [Lattice α] {s : Set α} : s ⊆ latticeClosure s

@[simp]

theorem isSublattice_latticeClosure {α : Type u_2} [Lattice α] {s : Set α} : IsSublattice (latticeClosure s)

theorem latticeClosure_min {α : Type u_2} [Lattice α] {s t : Set α} : s ⊆ t → IsSublattice t → latticeClosure s ⊆ t

theorem latticeClosure_mono {α : Type u_2} [Lattice α] : Monotone ⇑latticeClosure

@[simp]

theorem latticeClosure_eq_self {α : Type u_2} [Lattice α] {s : Set α} : latticeClosure s = s ↔ IsSublattice s

theorem IsSublattice.latticeClosure_eq {α : Type u_2} [Lattice α] {s : Set α} : IsSublattice s → latticeClosure s = s

Alias of the reverse direction of latticeClosure_eq_self.

theorem latticeClosure_idem {α : Type u_2} [Lattice α] (s : Set α) : latticeClosure (latticeClosure s) = latticeClosure s

@[simp]

theorem latticeClosure_empty {α : Type u_2} [Lattice α] : latticeClosure ∅ = ∅

@[simp]

theorem latticeClosure_singleton {α : Type u_2} [Lattice α] (a : α) : latticeClosure {a} = {a}

@[simp]

theorem latticeClosure_univ {α : Type u_2} [Lattice α] : latticeClosure Set.univ = Set.univ

theorem SupClosed.infClosure {α : Type u_2} [DistribLattice α] {s : Set α} (hs : SupClosed s) : SupClosed (infClosure s)

theorem InfClosed.supClosure {α : Type u_2} [DistribLattice α] {s : Set α} (hs : InfClosed s) : InfClosed (supClosure s)

@[simp]

theorem supClosure_infClosure {α : Type u_2} [DistribLattice α] (s : Set α) : supClosure (infClosure s) = latticeClosure s

@[simp]

theorem infClosure_supClosure {α : Type u_2} [DistribLattice α] (s : Set α) : infClosure (supClosure s) = latticeClosure s

theorem Set.Finite.latticeClosure {α : Type u_2} [DistribLattice α] {s : Set α} (hs : s.Finite) : (latticeClosure s).Finite

@[simp]

theorem latticeClosure_prod {α : Type u_2} {β : Type u_3} [DistribLattice α] [DistribLattice β] (s : Set α) (t : Set β) : latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t

def SemilatticeSup.toCompleteSemilatticeSup {α : Type u_2} [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

• SemilatticeSup.toCompleteSemilatticeSup sSup h = CompleteSemilatticeSup.mk ⋯ ⋯

def SemilatticeInf.toCompleteSemilatticeInf {α : Type u_2} [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

• SemilatticeInf.toCompleteSemilatticeInf sInf h = CompleteSemilatticeInf.mk ⋯ ⋯