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_2}
[SemilatticeSup α]
{s : Set α}
{t : Set α}
(hs : SupClosed s)
(ht : SupClosed t)
:
theorem
supClosed_sInter
{α : Type u_2}
[SemilatticeSup α]
{S : Set (Set α)}
(hS : ∀ s ∈ 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 (x x_1 : α) => x ≤ x_1) 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)
:
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)
:
theorem
supClosed_range
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[SemilatticeSup α]
[SemilatticeSup β]
[FunLike F α β]
[SupHomClass F α β]
(f : F)
:
theorem
SupClosed.prod
{α : Type u_2}
{β : Type u_3}
[SemilatticeSup α]
[SemilatticeSup β]
{s : Set α}
{t : Set β}
(hs : SupClosed s)
(ht : SupClosed 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))
:
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) → Finset.sup' t 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) → Finset.sup t f ∈ s
theorem
InfClosed.inter
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
{t : Set α}
(hs : InfClosed s)
(ht : InfClosed t)
:
theorem
infClosed_sInter
{α : Type u_2}
[SemilatticeInf α]
{S : Set (Set α)}
(hS : ∀ s ∈ 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 (x x_1 : α) => x ≥ x_1) 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)
:
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)
:
theorem
infClosed_range
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[SemilatticeInf α]
[SemilatticeInf β]
[FunLike F α β]
[InfHomClass F α β]
(f : F)
:
theorem
InfClosed.prod
{α : Type u_2}
{β : Type u_3}
[SemilatticeInf α]
[SemilatticeInf β]
{s : Set α}
{t : Set β}
(hs : InfClosed s)
(ht : InfClosed 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))
:
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) → Finset.inf' t 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) → Finset.inf t f ∈ 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.
Instances For
theorem
IsSublattice.inter
{α : Type u_2}
[Lattice α]
{s : Set α}
{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 (Set.pi s t)
@[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
Alias of the reverse direction of supClosed_preimage_ofDual.
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]
Closure #
@[simp]
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.
Instances For
@[simp]
@[simp]
theorem
supClosed_supClosure
{α : Type u_2}
[SemilatticeSup α]
{s : Set α}
:
SupClosed (supClosure s)
@[simp]
Alias of the reverse direction of supClosure_eq_self.
theorem
supClosure_idem
{α : Type u_2}
[SemilatticeSup α]
(s : Set α)
:
supClosure (supClosure s) = supClosure s
@[simp]
@[simp]
@[simp]
theorem
upperBounds_supClosure
{α : Type u_2}
[SemilatticeSup α]
(s : Set α)
:
upperBounds (supClosure s) = upperBounds s
@[simp]
theorem
sup_mem_supClosure
{α : Type u_2}
[SemilatticeSup α]
{s : Set α}
{a : α}
{b : α}
(ha : a ∈ s)
(hb : b ∈ 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)
:
Finset.sup' t ht f ∈ supClosure s
theorem
Set.Finite.supClosure
{α : Type u_2}
[SemilatticeSup α]
{s : Set α}
(hs : Set.Finite s)
:
Set.Finite (supClosure s)
The semilatice generated by a finite set is finite.
@[simp]
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.
Instances For
@[simp]
@[simp]
theorem
infClosed_infClosure
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
:
InfClosed (infClosure s)
@[simp]
Alias of the reverse direction of infClosure_eq_self.
theorem
infClosure_idem
{α : Type u_2}
[SemilatticeInf α]
(s : Set α)
:
infClosure (infClosure s) = infClosure s
@[simp]
@[simp]
@[simp]
theorem
lowerBounds_infClosure
{α : Type u_2}
[SemilatticeInf α]
(s : Set α)
:
lowerBounds (infClosure s) = lowerBounds s
@[simp]
theorem
inf_mem_infClosure
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
{a : α}
{b : α}
(ha : a ∈ s)
(hb : b ∈ 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)
:
Finset.inf' t ht f ∈ infClosure s
theorem
Set.Finite.infClosure
{α : Type u_2}
[SemilatticeInf α]
{s : Set α}
(hs : Set.Finite s)
:
Set.Finite (infClosure s)
The semilatice generated by a finite set is finite.
@[simp]
theorem
latticeClosure_isClosed
{α : Type u_2}
[Lattice α]
(s : Set α)
:
latticeClosure.IsClosed s = IsSublattice s
Every set in a join-semilattice generates a set closed under join.
Equations
- latticeClosure = ClosureOperator.ofCompletePred IsSublattice (_ : ∀ (x : Set (Set α)), (∀ s ∈ x, IsSublattice s) → IsSublattice (⋂₀ x))
Instances For
@[simp]
theorem
isSublattice_latticeClosure
{α : Type u_2}
[Lattice α]
{s : Set α}
:
IsSublattice (latticeClosure s)
theorem
latticeClosure_min
{α : Type u_2}
[Lattice α]
{s : Set α}
{t : Set α}
:
s ⊆ t → IsSublattice t → latticeClosure s ⊆ t
@[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.
@[simp]
@[simp]
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 : Set.Finite s)
:
Set.Finite (latticeClosure s)
def
SemilatticeSup.toCompleteSemilatticeSup
{α : Type u_2}
[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
- One or more equations did not get rendered due to their size.
Instances For
def
SemilatticeInf.toCompleteSemilatticeInf
{α : Type u_2}
[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.
Equations
- One or more equations did not get rendered due to their size.