Sets closed under countable join/meet

This file defines predicates for sets closed under countable ⊔ and dually for countable ⊓.

Main declarations

• CountableSupClosed: Predicate for a set to be closed under countable join.
• CountableInfClosed: Predicate for a set to be closed under countable meet.
• countableSupClosure: countable Sup-closure. Smallest countable sup-closed set containing a given set.
• countableInfClosure: countable Inf-closure. Smallest countable inf-closed set containing a given set.

Implementation notes

The list of properties in this file is copied and adapted from the file about SupClosed. We should keep these files in sync.

structure CountableSupClosed {α : Type u_2} [CompleteLattice α] (s : Set α) : Prop

A set s is countably sup-closed if ⨆ n, A n ∈ s for all A : ι → α with ι countable and A n ∈ s for all n.

The definition uses ι = ℕ and the empty case (⊥ ∈ s). See CountableSupClosed.iSup_mem for a supremum over any countable type.

• iSup_nat_mem ⦃A : ℕ → α⦄ (_hA : ∀ (n : ℕ), A n ∈ s) : ⨆ (n : ℕ), A n ∈ s

theorem CountableSupClosed.iSup_mem {ι : Sort u_1} {α : Type u_2} {s : Set α} [CompleteLattice α] [hι : Countable ι] [Nonempty ι] (hs : CountableSupClosed s) {A : ι → α} (hA : ∀ (n : ι), A n ∈ s) : ⨆ (n : ι), A n ∈ s

theorem CountableSupClosed.sSup_mem {α : Type u_2} {s : Set α} [CompleteLattice α] (hs : CountableSupClosed s) (A : Set α) [Countable ↑A] [Nonempty ↑A] (hA : ∀ a ∈ A, a ∈ s) : sSup A ∈ s

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

@[simp]

theorem countableSupClosed_singleton_bot {α : Type u_2} [CompleteLattice α] : CountableSupClosed {⊥}

@[simp]

theorem countableSupClosed_univ {α : Type u_2} [CompleteLattice α] : CountableSupClosed Set.univ

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

theorem countableSupClosed_sInter {α : Type u_2} {S : Set (Set α)} [CompleteLattice α] (hS : ∀ s ∈ S, CountableSupClosed s) : CountableSupClosed (⋂₀ S)

theorem countableSupClosed_iInter {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ι → Set α} (hf : ∀ (i : ι), CountableSupClosed (f i)) : CountableSupClosed (⋂ (i : ι), f i)

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

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

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

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

structure CountableInfClosed {α : Type u_2} [CompleteLattice α] (s : Set α) : Prop

A set s is countably inf-closed if ⨅ n, A n ∈ s for all A : ι → α with ι countable and A n ∈ s for all n.

The definition uses ι = ℕ and the empty case (⊤ ∈ s). See CountableInfClosed.iInf_mem for an infimum over any countable type.

• iInf_nat_mem ⦃A : ℕ → α⦄ : (∀ (n : ℕ), A n ∈ s) → ⨅ (n : ℕ), A n ∈ s

theorem CountableInfClosed.iInf_mem {ι : Sort u_1} {α : Type u_2} {s : Set α} [CompleteLattice α] [hι : Countable ι] [Nonempty ι] (hs : CountableInfClosed s) {A : ι → α} (hA : ∀ (n : ι), A n ∈ s) : ⨅ (n : ι), A n ∈ s

theorem CountableInfClosed.sInf_mem {α : Type u_2} {s : Set α} [CompleteLattice α] (hs : CountableInfClosed s) (A : Set α) [Countable ↑A] [Nonempty ↑A] (hA : ∀ a ∈ A, a ∈ s) : sInf A ∈ s

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

@[simp]

theorem countableInfClosed_singleton_top {α : Type u_2} [CompleteLattice α] : CountableInfClosed {⊤}

@[simp]

theorem countableInfClosed_univ {α : Type u_2} [CompleteLattice α] : CountableInfClosed Set.univ

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

theorem countableInfClosed_sInter {α : Type u_2} {S : Set (Set α)} [CompleteLattice α] (hS : ∀ s ∈ S, CountableInfClosed s) : CountableInfClosed (⋂₀ S)

theorem countableInfClosed_iInter {ι : Sort u_1} {α : Type u_2} [CompleteLattice α] {f : ι → Set α} (hf : ∀ (i : ι), CountableInfClosed (f i)) : CountableInfClosed (⋂ (i : ι), f i)

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

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

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

@[simp]

theorem countableSupClosed_preimage_toDual {α : Type u_2} [CompleteLattice α] {s : Set αᵒᵈ} : CountableSupClosed (⇑OrderDual.toDual ⁻¹' s) ↔ CountableInfClosed s

@[simp]

theorem countableInfClosed_preimage_toDual {α : Type u_2} [CompleteLattice α] {s : Set αᵒᵈ} : CountableInfClosed (⇑OrderDual.toDual ⁻¹' s) ↔ CountableSupClosed s

@[simp]

theorem countableSupClosed_preimage_ofDual {α : Type u_2} [CompleteLattice α] {s : Set α} : CountableSupClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ CountableInfClosed s

@[simp]

theorem countableInfClosed_preimage_ofDual {α : Type u_2} [CompleteLattice α] {s : Set α} : CountableInfClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ CountableSupClosed s

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

Alias of the reverse direction of countableSupClosed_preimage_ofDual.

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

Alias of the reverse direction of countableInfClosed_preimage_ofDual.

Closure

def countableSupClosure {α : Type u_2} [CompleteLattice α] : ClosureOperator (Set α)

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

Equations

• countableSupClosure = ClosureOperator.ofPred (fun (s : Set α) => {a : α | ∃ (t : ℕ → α), (∀ (n : ℕ), t n ∈ s) ∧ ⨆ (n : ℕ), t n = a}) CountableSupClosed ⋯ ⋯ ⋯

@[simp]

theorem countableSupClosure_isClosed {α : Type u_2} [CompleteLattice α] (s : Set α) : countableSupClosure.IsClosed s = CountableSupClosed s

theorem mem_countableSupClosure_iff {α : Type u_2} {s : Set α} {a : α} [CompleteLattice α] : a ∈ countableSupClosure s ↔ ∃ (t : ℕ → α), (∀ (n : ℕ), t n ∈ s) ∧ ⨆ (n : ℕ), t n = a

@[simp]

theorem subset_countableSupClosure {α : Type u_2} [CompleteLattice α] {s : Set α} : s ⊆ countableSupClosure s

@[simp]

theorem countableSupClosed_countableSupClosure {α : Type u_2} {s : Set α} [CompleteLattice α] : CountableSupClosed (countableSupClosure s)

@[simp]

theorem supClosed_countableSupClosure {α : Type u_2} {s : Set α} [CompleteLattice α] : SupClosed (countableSupClosure s)

theorem countableSupClosure_mono {α : Type u_2} [CompleteLattice α] : Monotone ⇑countableSupClosure

@[simp]

theorem countableSupClosure_eq_self {α : Type u_2} {s : Set α} [CompleteLattice α] : countableSupClosure s = s ↔ CountableSupClosed s

theorem CountableSupClosed.countableSupClosure_eq {α : Type u_2} {s : Set α} [CompleteLattice α] : CountableSupClosed s → countableSupClosure s = s

Alias of the reverse direction of countableSupClosure_eq_self.

theorem countableSupClosure_idem {α : Type u_2} [CompleteLattice α] (s : Set α) : countableSupClosure (countableSupClosure s) = countableSupClosure s

@[simp]

theorem countableSupClosure_singleton_bot {α : Type u_2} [CompleteLattice α] : countableSupClosure {⊥} = {⊥}

@[simp]

theorem countableSupClosure_univ {α : Type u_2} [CompleteLattice α] : countableSupClosure Set.univ = Set.univ

@[simp]

theorem upperBounds_countableSupClosure {α : Type u_2} [CompleteLattice α] (s : Set α) : upperBounds (countableSupClosure s) = upperBounds s

@[simp]

theorem isLUB_countableSupClosure {α : Type u_2} {s : Set α} {a : α} [CompleteLattice α] : IsLUB (countableSupClosure s) a ↔ IsLUB s a

theorem sup_mem_countableSupClosure {α : Type u_2} {s : Set α} {a b : α} [CompleteLattice α] (ha : a ∈ s) (hb : b ∈ s) : a ⊔ b ∈ countableSupClosure s

theorem iSup_mem_countableSupClosure {ι : Sort u_1} {α : Type u_2} {s : Set α} [CompleteLattice α] [Countable ι] [Nonempty ι] {A : ι → α} (hA : ∀ (n : ι), A n ∈ s) : ⨆ (n : ι), A n ∈ countableSupClosure s

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

theorem countableSupClosure_min {α : Type u_2} {s t : Set α} [CompleteLattice α] : s ⊆ t → CountableSupClosed t → countableSupClosure s ⊆ t

@[simp]

theorem countableSupClosure_prod {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (s : Set α) (t : Set β) : countableSupClosure (s ×ˢ t) = countableSupClosure s ×ˢ countableSupClosure t

def countableInfClosure {α : Type u_2} [CompleteLattice α] : ClosureOperator (Set α)

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

Equations

• countableInfClosure = ClosureOperator.ofPred (fun (s : Set α) => {a : α | ∃ (t : ℕ → α), (∀ (n : ℕ), t n ∈ s) ∧ ⨅ (n : ℕ), t n = a}) CountableInfClosed ⋯ ⋯ ⋯

@[simp]

theorem countableInfClosure_isClosed {α : Type u_2} [CompleteLattice α] (s : Set α) : countableInfClosure.IsClosed s = CountableInfClosed s

theorem mem_countableInfClosure_iff {α : Type u_2} {s : Set α} {a : α} [CompleteLattice α] : a ∈ countableInfClosure s ↔ ∃ (t : ℕ → α), (∀ (n : ℕ), t n ∈ s) ∧ ⨅ (n : ℕ), t n = a

@[simp]

theorem subset_countableInfClosure {α : Type u_2} [CompleteLattice α] {s : Set α} : s ⊆ countableInfClosure s

@[simp]

theorem countableInfClosed_countableInfClosure {α : Type u_2} {s : Set α} [CompleteLattice α] : CountableInfClosed (countableInfClosure s)

@[simp]

theorem infClosed_countableInfClosure {α : Type u_2} {s : Set α} [CompleteLattice α] : InfClosed (countableInfClosure s)

theorem countableInfClosure_mono {α : Type u_2} [CompleteLattice α] : Monotone ⇑countableInfClosure

@[simp]

theorem countableInfClosure_eq_self {α : Type u_2} {s : Set α} [CompleteLattice α] : countableInfClosure s = s ↔ CountableInfClosed s

theorem CountableInfClosed.countableInfClosure_eq {α : Type u_2} {s : Set α} [CompleteLattice α] : CountableInfClosed s → countableInfClosure s = s

Alias of the reverse direction of countableInfClosure_eq_self.

theorem countableInfClosure_idem {α : Type u_2} [CompleteLattice α] (s : Set α) : countableInfClosure (countableInfClosure s) = countableInfClosure s

@[simp]

theorem countableInfClosure_singleton_top {α : Type u_2} [CompleteLattice α] : countableInfClosure {⊤} = {⊤}

@[simp]

theorem countableInfClosure_univ {α : Type u_2} [CompleteLattice α] : countableInfClosure Set.univ = Set.univ

@[simp]

theorem lowerBounds_countableInfClosure {α : Type u_2} [CompleteLattice α] (s : Set α) : lowerBounds (countableInfClosure s) = lowerBounds s

@[simp]

theorem isGLB_countableInfClosure {α : Type u_2} {s : Set α} {a : α} [CompleteLattice α] : IsGLB (countableInfClosure s) a ↔ IsGLB s a

theorem inf_mem_countableInfClosure {α : Type u_2} {s : Set α} {a b : α} [CompleteLattice α] (ha : a ∈ s) (hb : b ∈ s) : a ⊓ b ∈ countableInfClosure s

theorem iInf_mem_countableInfClosure {ι : Sort u_1} {α : Type u_2} {s : Set α} [CompleteLattice α] [Countable ι] [Nonempty ι] {A : ι → α} (hA : ∀ (n : ι), A n ∈ s) : ⨅ (n : ι), A n ∈ countableInfClosure s

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

theorem countableInfClosure_min {α : Type u_2} {s t : Set α} [CompleteLattice α] : s ⊆ t → CountableInfClosed t → countableInfClosure s ⊆ t

@[simp]

theorem countableInfClosure_prod {α : Type u_2} {β : Type u_3} [CompleteLattice α] [CompleteLattice β] (s : Set α) (t : Set β) : countableInfClosure (s ×ˢ t) = countableInfClosure s ×ˢ countableInfClosure t

theorem SupClosed.countableInfClosure {α : Type u_2} {s : Set α} [Order.Coframe α] (hs : SupClosed s) : SupClosed (countableInfClosure s)

theorem InfClosed.countableSupClosure {α : Type u_2} {s : Set α} [Order.Frame α] (hs : InfClosed s) : InfClosed (countableSupClosure s)