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 ∈ sandb ∈ simplya ⊔ b ∈ s).InfClosed: Predicate for a set to be closed under meet (a ∈ sandb ∈ simplya ⊓ 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.
theorem
SupClosed.inter
{α : Type u_3}
[SemilatticeSup α]
{s t : Set α}
(hs : SupClosed s)
(ht : SupClosed t)
:
theorem
supClosed_sInter
{α : Type u_3}
[SemilatticeSup α]
{S : Set (Set α)}
(hS : ∀ s ∈ S, SupClosed s)
:
theorem
supClosed_iInter
{α : Type u_3}
[SemilatticeSup α]
{ι : Sort u_5}
{f : ι → Set α}
(hf : ∀ (i : ι), SupClosed (f i))
:
SupClosed (⋂ (i : ι), f i)
theorem
SupClosed.directedOn
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
(hs : SupClosed s)
:
DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s
theorem
SupClosed.preimage
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[SemilatticeSup α]
[SemilatticeSup β]
{s : Set α}
[FunLike F β α]
[SupHomClass F β α]
(hs : SupClosed s)
(f : F)
:
theorem
SupClosed.image
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[SemilatticeSup α]
[SemilatticeSup β]
{s : Set α}
[FunLike F α β]
[SupHomClass F α β]
(hs : SupClosed s)
(f : F)
:
theorem
supClosed_range
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[SemilatticeSup α]
[SemilatticeSup β]
[FunLike F α β]
[SupHomClass F α β]
(f : F)
:
theorem
SupClosed.prod
{α : Type u_3}
{β : Type u_4}
[SemilatticeSup α]
[SemilatticeSup β]
{s : Set α}
{t : Set β}
(hs : SupClosed s)
(ht : SupClosed t)
:
theorem
supClosed_pi
{ι : Type u_6}
{α : ι → Type u_7}
[(i : ι) → SemilatticeSup (α i)]
{s : Set ι}
{t : (i : ι) → Set (α i)}
(ht : ∀ i ∈ s, SupClosed (t i))
:
theorem
SupClosed.insert_upperBounds
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
{a : α}
(hs : SupClosed s)
(ha : a ∈ upperBounds s)
:
theorem
SupClosed.insert_lowerBounds
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
{a : α}
(h : SupClosed s)
(ha : a ∈ lowerBounds s)
:
theorem
InfClosed.inter
{α : Type u_3}
[SemilatticeInf α]
{s t : Set α}
(hs : InfClosed s)
(ht : InfClosed t)
:
theorem
infClosed_sInter
{α : Type u_3}
[SemilatticeInf α]
{S : Set (Set α)}
(hS : ∀ s ∈ S, InfClosed s)
:
theorem
infClosed_iInter
{α : Type u_3}
[SemilatticeInf α]
{ι : Sort u_5}
{f : ι → Set α}
(hf : ∀ (i : ι), InfClosed (f i))
:
InfClosed (⋂ (i : ι), f i)
theorem
InfClosed.codirectedOn
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
(hs : InfClosed s)
:
DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s
theorem
InfClosed.preimage
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[SemilatticeInf α]
[SemilatticeInf β]
{s : Set α}
[FunLike F β α]
[InfHomClass F β α]
(hs : InfClosed s)
(f : F)
:
theorem
InfClosed.image
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[SemilatticeInf α]
[SemilatticeInf β]
{s : Set α}
[FunLike F α β]
[InfHomClass F α β]
(hs : InfClosed s)
(f : F)
:
theorem
infClosed_range
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[SemilatticeInf α]
[SemilatticeInf β]
[FunLike F α β]
[InfHomClass F α β]
(f : F)
:
theorem
InfClosed.prod
{α : Type u_3}
{β : Type u_4}
[SemilatticeInf α]
[SemilatticeInf β]
{s : Set α}
{t : Set β}
(hs : InfClosed s)
(ht : InfClosed t)
:
theorem
infClosed_pi
{ι : Type u_6}
{α : ι → Type u_7}
[(i : ι) → SemilatticeInf (α i)]
{s : Set ι}
{t : (i : ι) → Set (α i)}
(ht : ∀ i ∈ s, InfClosed (t i))
:
theorem
InfClosed.insert_upperBounds
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
{a : α}
(hs : InfClosed s)
(ha : a ∈ upperBounds s)
:
theorem
InfClosed.insert_lowerBounds
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
{a : α}
(h : InfClosed s)
(ha : a ∈ lowerBounds s)
:
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.
theorem
IsSublattice.inter
{α : Type u_3}
[Lattice α]
{s t : Set α}
(hs : IsSublattice s)
(ht : IsSublattice t)
:
IsSublattice (s ∩ t)
theorem
isSublattice_sInter
{α : Type u_3}
[Lattice α]
{S : Set (Set α)}
(hS : ∀ s ∈ S, IsSublattice s)
:
IsSublattice (⋂₀ S)
theorem
isSublattice_iInter
{α : Type u_3}
{ι : Sort u_5}
[Lattice α]
{f : ι → Set α}
(hf : ∀ (i : ι), IsSublattice (f i))
:
IsSublattice (⋂ (i : ι), f i)
theorem
IsSublattice.preimage
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[Lattice α]
[Lattice β]
{s : Set α}
[FunLike F β α]
[LatticeHomClass F β α]
(hs : IsSublattice s)
(f : F)
:
IsSublattice (⇑f ⁻¹' s)
theorem
IsSublattice.image
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[Lattice α]
[Lattice β]
{s : Set α}
[FunLike F α β]
[LatticeHomClass F α β]
(hs : IsSublattice s)
(f : F)
:
IsSublattice (⇑f '' s)
theorem
IsSublattice_range
{F : Type u_2}
{α : Type u_3}
{β : Type u_4}
[Lattice α]
[Lattice β]
[FunLike F α β]
[LatticeHomClass F α β]
(f : F)
:
IsSublattice (Set.range ⇑f)
theorem
IsSublattice.prod
{α : Type u_3}
{β : Type u_4}
[Lattice α]
[Lattice β]
{s : Set α}
{t : Set β}
(hs : IsSublattice s)
(ht : IsSublattice t)
:
IsSublattice (s ×ˢ t)
theorem
isSublattice_pi
{ι : Type u_6}
{α : ι → Type u_7}
[(i : ι) → Lattice (α i)]
{s : Set ι}
{t : (i : ι) → Set (α i)}
(ht : ∀ i ∈ s, IsSublattice (t i))
:
IsSublattice (s.pi t)
@[simp]
@[simp]
@[simp]
@[simp]
theorem
InfClosed.dual
{α : Type u_3}
[Lattice α]
{s : Set α}
:
InfClosed s → SupClosed (⇑OrderDual.ofDual ⁻¹' s)
Alias of the reverse direction of supClosed_preimage_ofDual.
theorem
SupClosed.dual
{α : Type u_3}
[Lattice α]
{s : Set α}
:
SupClosed s → InfClosed (⇑OrderDual.ofDual ⁻¹' s)
Alias of the reverse direction of infClosed_preimage_ofDual.
theorem
IsSublattice.dual
{α : Type u_3}
[Lattice α]
{s : Set α}
:
IsSublattice s → IsSublattice (⇑OrderDual.ofDual ⁻¹' s)
Alias of the reverse direction of isSublattice_preimage_ofDual.
theorem
IsSublattice.of_dual
{α : Type u_3}
[Lattice α]
{s : Set αᵒᵈ}
:
IsSublattice s → IsSublattice (⇑OrderDual.toDual ⁻¹' s)
Alias of the reverse direction of isSublattice_preimage_toDual.
@[simp]
Closure #
Every set in a join-semilattice generates a set closed under join.
@[simp]
@[simp]
@[simp]
theorem
supClosed_supClosure
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
:
SupClosed (supClosure s)
@[simp]
theorem
SupClosed.supClosure_eq
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
:
SupClosed s → supClosure s = s
Alias of the reverse direction of supClosure_eq_self.
@[simp]
@[simp]
@[simp]
@[simp]
theorem
sup_mem_supClosure
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
{a b : α}
(ha : a ∈ s)
(hb : b ∈ s)
:
theorem
finsetSup'_mem_supClosure
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
{ι : Type u_5}
{t : Finset ι}
(ht : t.Nonempty)
{f : ι → α}
(hf : ∀ i ∈ t, f i ∈ s)
:
theorem
supClosure_min
{α : Type u_3}
[SemilatticeSup α]
{s t : Set α}
:
s ⊆ t → SupClosed t → supClosure s ⊆ t
theorem
Set.Finite.supClosure
{α : Type u_3}
[SemilatticeSup α]
{s : Set α}
(hs : s.Finite)
:
(supClosure s).Finite
The semilatice generated by a finite set is finite.
@[simp]
theorem
supClosure_prod
{α : Type u_3}
{β : Type u_4}
[SemilatticeSup α]
[SemilatticeSup β]
(s : Set α)
(t : Set β)
:
Every set in a join-semilattice generates a set closed under join.
@[simp]
@[simp]
@[simp]
theorem
infClosed_infClosure
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
:
InfClosed (infClosure s)
@[simp]
theorem
InfClosed.infClosure_eq
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
:
InfClosed s → infClosure s = s
Alias of the reverse direction of infClosure_eq_self.
@[simp]
@[simp]
@[simp]
@[simp]
theorem
inf_mem_infClosure
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
{a b : α}
(ha : a ∈ s)
(hb : b ∈ s)
:
theorem
finsetInf'_mem_infClosure
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
{ι : Type u_5}
{t : Finset ι}
(ht : t.Nonempty)
{f : ι → α}
(hf : ∀ i ∈ t, f i ∈ s)
:
theorem
infClosure_min
{α : Type u_3}
[SemilatticeInf α]
{s t : Set α}
:
s ⊆ t → InfClosed t → infClosure s ⊆ t
theorem
Set.Finite.infClosure
{α : Type u_3}
[SemilatticeInf α]
{s : Set α}
(hs : s.Finite)
:
(infClosure s).Finite
The semilatice generated by a finite set is finite.
@[simp]
theorem
infClosure_prod
{α : Type u_3}
{β : Type u_4}
[SemilatticeInf α]
[SemilatticeInf β]
(s : Set α)
(t : Set β)
:
Every set in a join-semilattice generates a set closed under join.
@[simp]
@[simp]
@[simp]
theorem
latticeClosure_min
{α : Type u_3}
[Lattice α]
{s t : Set α}
:
s ⊆ t → IsSublattice t → latticeClosure s ⊆ t
@[simp]
theorem
IsSublattice.latticeClosure_eq
{α : Type u_3}
[Lattice α]
{s : Set α}
:
IsSublattice s → latticeClosure s = s
Alias of the reverse direction of latticeClosure_eq_self.
@[simp]
@[simp]
theorem
SupClosed.infClosure
{α : Type u_3}
[DistribLattice α]
{s : Set α}
(hs : SupClosed s)
:
SupClosed (infClosure s)
theorem
InfClosed.supClosure
{α : Type u_3}
[DistribLattice α]
{s : Set α}
(hs : InfClosed s)
:
InfClosed (supClosure s)
@[simp]
@[simp]
@[simp]
theorem
latticeClosure_prod
{α : Type u_3}
{β : Type u_4}
[DistribLattice α]
[DistribLattice β]
(s : Set α)
(t : Set β)
:
def
SemilatticeSup.toCompleteSemilatticeSup
{α : Type u_3}
[SemilatticeSup α]
(sSup : Set α → α)
(h : ∀ (s : Set α), SupClosed s → IsLUB s (sSup s))
:
A join-semilattice where every sup-closed set has a least upper bound is automatically complete.
Equations
def
SemilatticeInf.toCompleteSemilatticeInf
{α : Type u_3}
[SemilatticeInf α]
(sInf : Set α → α)
(h : ∀ (s : Set α), InfClosed s → IsGLB s (sInf s))
:
A meet-semilattice where every inf-closed set has a greatest lower bound is automatically complete.