Suprema of pointwise sups

Mirror of Mathlib/Data/Set/Sups.lean. Pointwise sups preserve sup-closure and the bottom element in any semilattice, and downward closure and order-convexity (the latter given sup-closure) in a distributive lattice, where c ≤ a ⊔ b splits as c = (c ⊓ a) ⊔ (c ⊓ b). In a complete lattice, the supremum of s ⊻ t is the join of the suprema of two nonempty sets. The indexed form of s ⊻ t is Set.iSups s, the set of suprema of choices of an element from each member of a family s. [UPSTREAM]

theorem SupClosed.sups {α : Type u_1} [SemilatticeSup α] {s t : Set α} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ⊻ t)

theorem Set.bot_mem_sups {α : Type u_1} [SemilatticeSup α] {s t : Set α} [OrderBot α] (hs : ⊥ ∈ s) (ht : ⊥ ∈ t) : ⊥ ∈ s ⊻ t

theorem IsLowerSet.sups {α : Type u_1} [DistribLattice α] {s t : Set α} (hs : IsLowerSet s) (ht : IsLowerSet t) : IsLowerSet (s ⊻ t)

theorem Set.OrdConnected.sups {α : Type u_1} [DistribLattice α] {s t : Set α} (hs : s.OrdConnected) (ht : t.OrdConnected) (hs' : SupClosed s) (ht' : SupClosed t) : (s ⊻ t).OrdConnected

Pointwise sups of convex sets are convex when both sets are sup-closed: an element x between a ⊔ b and c ⊔ d splits as (a ⊔ c) ⊓ x ⊔ (b ⊔ d) ⊓ x, each part lying between a and a ⊔ c, respectively b and b ⊔ d.

theorem Set.sSup_sups {α : Type u_1} [CompleteLattice α] {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) : sSup (s ⊻ t) = sSup s ⊔ sSup t

The supremum of s ⊻ t is sSup s ⊔ sSup t when s and t are nonempty. [UPSTREAM]

def Set.iSups {α : Type u_1} [CompleteLattice α] {ι : Type u_2} (s : ι → Set α) : Set α

The pointwise supremum of a family of sets is the set of suprema of choices of an element from each member of the family. [UPSTREAM]

Equations

• Set.iSups s = (fun (f : ι → α) => ⨆ (i : ι), f i) '' Set.univ.pi s

theorem Set.mem_iSups {α : Type u_1} [CompleteLattice α] {ι : Type u_2} {s : ι → Set α} {a : α} : a ∈ iSups s ↔ ∃ (f : ι → α), (∀ (i : ι), f i ∈ s i) ∧ ⨆ (i : ι), f i = a

theorem Set.iSup_mem_iSups {α : Type u_1} [CompleteLattice α] {ι : Type u_2} {s : ι → Set α} {f : ι → α} (hf : ∀ (i : ι), f i ∈ s i) : ⨆ (i : ι), f i ∈ iSups s

theorem Set.exists_mem_iSups_ge {α : Type u_1} [CompleteLattice α] {ι : Type u_2} {s : ι → Set α} {a : α} (hs : ∀ (j : ι), (s j).Nonempty) {i : ι} (ha : a ∈ s i) : ∃ b ∈ iSups s, a ≤ b

An element of one member of a family of nonempty sets lies below an element of their pointwise supremum. [UPSTREAM]

theorem Set.sSup_iSups {α : Type u_1} [CompleteLattice α] {ι : Type u_2} {s : ι → Set α} (hs : ∀ (i : ι), (s i).Nonempty) : sSup (iSups s) = ⨆ (i : ι), sSup (s i)

The supremum of Set.iSups s is the supremum of the suprema of the s i when each is nonempty. [UPSTREAM]

theorem Set.upperClosure_iSups {α : Type u_1} [CompleteLattice α] {ι : Type u_2} {s : ι → Set α} : upperClosure (iSups s) = ⨆ (i : ι), upperClosure (s i)

The upper closure of Set.iSups s is the meet of the upper closures of the s i, as upper sets. [UPSTREAM]