# 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

Instances
class InfSet (α : Type u_1) :
Type u_1

Class for the sInf operator

• sInf : Set αα

Infimum of a set

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

Indexed supremum

Equations
Instances For
def iInf {α : Type u} {ι : Sort v} [] (s : ια) :
α

Indexed infimum

Equations
Instances For
@[instance 50]
instance infSet_to_nonempty (α : Type u_1) [] :
Equations
• =
@[instance 50]
instance supSet_to_nonempty (α : Type u_1) [] :
Equations
• =

Indexed supremum.

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

Pretty printer defined by notation3 command.

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

Indexed infimum.

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

Pretty printer defined by notation3 command.

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

Delaborator for indexed supremum.

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

Delaborator for indexed infimum.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Set.instInfSet {α : Type u} :
InfSet (Set α)
Equations
• Set.instInfSet = { sInf := fun (s : Set (Set α)) => {a : α | ∀ (t : Set α), t sa 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
Instances For

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

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

Union of a set of sets.

Equations
Instances For

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

Equations
Instances For
@[simp]
theorem Set.mem_sInter {α : Type u} {x : α} {S : Set (Set α)} :
x ⋂₀ S ∀ (t : Set α), t Sx 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
Instances For
def Set.iInter {α : Type u} {ι : Sort v} (s : ιSet α) :
Set α

Indexed intersection of a family of sets

Equations
Instances For

Pretty printer defined by notation3 command.

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

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

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

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

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

Pretty printer defined by notation3 command.

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

Delaborator for indexed unions.

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

Delaborator for indexed intersections.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[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 α)) :
@[simp]
theorem Set.sInf_eq_sInter {α : Type u} (S : Set (Set α)) :
@[simp]
theorem Set.iSup_eq_iUnion {α : Type u} {ι : Sort v} (s : ιSet α) :
iSup s =
@[simp]
theorem Set.iInf_eq_iInter {α : Type u} {ι : Sort v} (s : ιSet α) :
iInf s =