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

Equations

• iSup s = sSup (Set.range s)

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

Indexed infimum

Equations

• iInf s = sInf (Set.range s)

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

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

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

Indexed supremum.

Equations

• One or more equations did not get rendered due to their size.

def «term⨆_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term⨅_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

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

Indexed infimum.

Equations

• One or more equations did not get rendered due to their size.

def iSup_delab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for indexed supremum.

Equations

• One or more equations did not get rendered due to their size.

def iInf_delab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for indexed infimum.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Set.instInfSet = { sInf := fun (s : Set (Set α)) => {a : α | ∀ (t : Set α), t ∈ s → a ∈ t} }

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

Equations

• Set.instSupSet = { sSup := fun (s : Set (Set α)) => {a : α | ∃ (t : Set α), t ∈ s ∧ a ∈ t} }

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

Intersection of a set of sets.

Equations

• ⋂₀ S = sInf S

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

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

Equations

• Set.«term⋂₀_» = Lean.ParserDescr.node `Set.«term⋂₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

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

Union of a set of sets.

Equations

• ⋃₀ S = sSup S

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

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

Equations

• Set.«term⋃₀_» = Lean.ParserDescr.node `Set.«term⋃₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

@[simp]

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

@[simp]

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

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

Indexed union of a family of sets

Equations

• Set.iUnion s = iSup s

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

Indexed intersection of a family of sets

Equations

• Set.iInter s = iInf s

def Set.«term⋃_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

def Set.«term⋂_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

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

Delaborator for indexed unions.

Equations

• One or more equations did not get rendered due to their size.

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

Delaborator for indexed intersections.

Equations

• One or more equations did not get rendered due to their size.

@[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 = Set.iUnion s

@[simp]

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