Notation classes for set supremum and infimum

In this file we introduce notation for indexed suprema, infima, unions, and intersections.

Main definitions

• SupSet α: typeclass introducing the operation SupSet.sSup (exported to the root namespace); sSup s is the supremum of the set s;
• InfSet: similar typeclass for infimum of a set;
• iSup f, iInf f: supremum and infimum of an indexed family of elements, defined as sSup (Set.range f) and sInf (Set.range f), respectively;
• Set.sUnion s, Set.sInter s: same as sSup s and sInf s, but works only for sets of sets;
• Set.iUnion s, Set.iInter s: same as iSup s and iInf s, but works only for indexed families of sets.

Notation

• ⨆ i, f i, ⨅ i, f i: supremum and infimum of an indexed family, respectively;
• ⋃₀ s, ⋂₀ s: union and intersection of a set of sets;
• ⋃ i, s i, ⋂ i, s i: union and intersection of an indexed family of sets.

class SupSet (α : Type u_1) : Type u_1

Class for the sSup operator

• sSup : Set α → α

  Supremum of a set

class InfSet (α : Type u_1) : Type u_1

Class for the sInf operator

• sInf : Set α → α

  Infimum of a set

def iSup {α : Type u} {ι : Sort v} [SupSet α] (s : ι → α) : α

Indexed supremum

def iInf {α : Type u} {ι : Sort v} [InfSet α] (s : ι → α) : α

Indexed infimum

@[instance 50]

instance infSet_to_nonempty (α : Type u_1) [InfSet α] : Nonempty α

@[instance 50]

instance supSet_to_nonempty (α : Type u_1) [SupSet α] : Nonempty α

def «term⨆_,_» : Lean.ParserDescr

Indexed supremum.

def «term⨅_,_» : Lean.ParserDescr

Indexed infimum.

def iSup_delab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for indexed supremum.

def iInf_delab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for indexed infimum.

@[implicit_reducible]

instance Set.instInfSet {α : Type u} : InfSet (Set α)

@[implicit_reducible]

instance Set.instSupSet {α : Type u} : SupSet (Set α)

def Set.sInter {α : Type u} (S : Set (Set α)) : Set α

Intersection of a set of sets.

def Set.«term⋂₀_» : Lean.ParserDescr

Notation for Set.sInter Intersection of a set of sets.

def Set.sUnion {α : Type u} (S : Set (Set α)) : Set α

Union of a set of sets.

def Set.«term⋃₀_» : Lean.ParserDescr

Notation for Set.sUnion. Union of a set of sets.

@[simp]

theorem Set.mem_sInter {α : Type u} {x : α} {S : Set (Set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t

@[simp]

theorem Set.mem_sUnion {α : Type u} {x : α} {S : Set (Set α)} : x ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t

def Set.iUnion {α : Type u} {ι : Sort v} (s : ι → Set α) : Set α

Indexed union of a family of sets

def Set.iInter {α : Type u} {ι : Sort v} (s : ι → Set α) : Set α

Indexed intersection of a family of sets

def Set.«term⋃_,_» : Lean.ParserDescr

Notation for Set.iUnion. Indexed union of a family of sets

def Set.«term⋂_,_» : Lean.ParserDescr

Notation for Set.iInter. Indexed intersection of a family of sets

def Set.iUnion_delab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for indexed unions.

def Set.sInter_delab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for indexed intersections.

@[simp]

theorem Set.mem_iUnion {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α} : x ∈ ⋃ (i : ι), s i ↔ ∃ (i : ι), x ∈ s i

@[simp]

theorem Set.mem_iInter {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α} : x ∈ ⋂ (i : ι), s i ↔ ∀ (i : ι), x ∈ s i

@[simp]

theorem Set.sSup_eq_sUnion {α : Type u} (S : Set (Set α)) : sSup S = ⋃₀ S

@[simp]

theorem Set.sInf_eq_sInter {α : Type u} (S : Set (Set α)) : sInf S = ⋂₀ S

@[simp]

theorem Set.iSup_eq_iUnion {α : Type u} {ι : Sort v} (s : ι → Set α) : iSup s = iUnion s

@[simp]

theorem Set.iInf_eq_iInter {α : Type u} {ι : Sort v} (s : ι → Set α) : iInf s = iInter s