Sets closed under countable join/meet

This file defines predicates for sets closed under countable supremum and dually for countable infimum.

Main declarations

• CountableSupClosed: Predicate for a set to be closed under countable supremum.
• CountableInfClosed: Predicate for a set to be closed under countable infimum.
• 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} [LE α] (s : Set α) : Prop

A set s is closed under countable supremum if for every nonempty countable subset of s, any least upper bound of that subset is in s.

• isLUB_mem (t : Set α) : t ⊆ s → t.Nonempty → t.Countable → ∀ (x : α), IsLUB t x → x ∈ s

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

A set s is closed under countable infimum if for every nonempty countable subset of s, any greatest lower bound of that subset is in s.

• isGLB_mem (t : Set α) : t ⊆ s → t.Nonempty → t.Countable → ∀ (x : α), IsGLB t x → x ∈ s

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

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

theorem CountableSupClosed.of_iSup_mem {α : Type u_2} {s : Set α} [CompleteLattice α] (hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ (n : ℕ), A n ∈ s) : CountableSupClosed s

theorem CountableInfClosed.of_iInf_mem {α : Type u_2} {s : Set α} [CompleteLattice α] (hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨅ (n : ℕ), A n ∈ s) : CountableInfClosed s

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

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

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

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

@[simp]

theorem CountableSupClosed.singleton {α : Type u_2} [PartialOrder α] {x : α} : CountableSupClosed {x}

@[simp]

theorem CountableInfClosed.singleton {α : Type u_2} [PartialOrder α] {x : α} : CountableInfClosed {x}

@[simp]

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

@[simp]

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

@[simp]

theorem CountableSupClosed.empty {α : Type u_2} [LE α] : CountableSupClosed ∅

@[simp]

theorem CountableInfClosed.empty {α : Type u_2} [LE α] : CountableInfClosed ∅

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of countableInfClosed_preimage_ofDual.

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

Closure

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

Every set generates a set closed under countable supremum.

Equations

• countableSupClosure = ClosureOperator.ofPred (fun (s : Set α) (a : α) => ∃ (A : Set α) (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a) CountableSupClosed ⋯ ⋯ ⋯

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

Every set generates a set closed under countable infimum.

Equations

• countableInfClosure = ClosureOperator.ofPred (fun (s : Set α) (a : α) => ∃ (A : Set α) (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsGLB A a) CountableInfClosed ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

theorem countableSupClosure_min {α : Type u_2} {s t : Set α} [Preorder α] (hst : s ⊆ t) (ht : CountableSupClosed t) : countableSupClosure s ⊆ t

theorem countableInfClosure_min {α : Type u_2} {s t : Set α} [Preorder α] (hst : s ⊆ t) (ht : CountableInfClosed t) : countableInfClosure s ⊆ t

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of countableSupClosure_eq_self.

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

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

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

theorem countableSupClosure_eq_sInter {α : Type u_2} [Preorder α] (s : Set α) : countableSupClosure s = ⋂₀ {t : Set α | s ⊆ t ∧ CountableSupClosed t}

theorem countableInfClosure_eq_sInter {α : Type u_2} [Preorder α] (s : Set α) : countableInfClosure s = ⋂₀ {t : Set α | s ⊆ t ∧ CountableInfClosed t}

theorem mem_countableSupClosure_iff {α : Type u_2} {s : Set α} {a : α} [Preorder α] : a ∈ countableSupClosure s ↔ ∃ (A : Set α) (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a

theorem mem_countableInfClosure_iff {α : Type u_2} {s : Set α} {a : α} [Preorder α] : a ∈ countableInfClosure s ↔ ∃ (A : Set α) (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsGLB A a

@[simp]

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

@[simp]

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

@[simp]

theorem countableSupClosure_empty {α : Type u_2} [Preorder α] : countableSupClosure ∅ = ∅

@[simp]

theorem countableInfClosure_empty {α : Type u_2} [Preorder α] : countableInfClosure ∅ = ∅

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem countableSupClosure_singleton {α : Type u_2} [PartialOrder α] {x : α} : countableSupClosure {x} = {x}

@[simp]

theorem countableInfClosure_singleton {α : Type u_2} [PartialOrder α] {x : α} : countableInfClosure {x} = {x}

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

theorem inf_mem_countableInfClosure {α : Type u_2} {s : Set α} {a b : α} [SemilatticeInf α] (ha : a ∈ s) (hb : b ∈ s) : a ⊓ b ∈ countableInfClosure 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 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 finsetSup'_mem_countableSupClosure {α : Type u_2} {s : Set α} {ι : Type u_4} [SemilatticeSup α] {t : Finset ι} (ht : t.Nonempty) {f : ι → α} (hf : ∀ i ∈ t, f i ∈ s) : t.sup' ht f ∈ countableSupClosure s

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

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

If a set is closed under binary suprema, then its countable infimum closure is also closed under binary suprema.

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

If a set is closed under binary infima, then its countable supremum closure is also closed under binary infima.