Documentation

Mathlib.Order.SetNotation

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} [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)

@[instance 50]

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

Equations

⋯ = ⋯

@[instance 50]

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

Equations

⋯ = ⋯

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

Instances For

Set.ordConnected_iInter'

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