Mathlib.Order.SetNotation

SupSet structure

(α : Type*)

Full source

/-- Class for the `sSup` operator -/
class SupSet (α : Type*) where
  /-- Supremum of a set -/
  sSup : Set α → α

Supremum operator for sets

Informal description

The structure `SupSet` is a typeclass that introduces the supremum operator `sSup` for a type `α`, where `sSup s` denotes the supremum of a set `s` in `α`.

InfSet structure

(α : Type*)

Full source

/-- Class for the `sInf` operator -/
class InfSet (α : Type*) where
  /-- Infimum of a set -/
  sInf : Set α → α

Infimum structure

Informal description

The structure `InfSet` introduces the infimum operator `sInf` for a type `α`, which computes the greatest lower bound of a set of elements in `α`.

iSup definition

[SupSet α] (s : ι → α) : α

Full source

/-- Indexed supremum -/
def iSup [SupSet α] (s : ι → α) : α :=
  sSup (range s)

Indexed supremum $\bigsqcup_i s_i$

Informal description

For a type $\alpha$ equipped with a supremum structure and an indexed family $s : \iota \to \alpha$, the term $\bigsqcup_i s_i$ denotes the supremum (least upper bound) of the range of $s$. This is defined as $\mathrm{sSup}(\mathrm{range}\, s)$.

iInf definition

[InfSet α] (s : ι → α) : α

Full source

/-- Indexed infimum -/
def iInf [InfSet α] (s : ι → α) : α :=
  sInf (range s)

Indexed infimum $\bigsqcap_i s_i$

Informal description

For a type $\alpha$ equipped with an infimum structure and an indexed family $s : \iota \to \alpha$, the term $\bigsqcap_i s_i$ denotes the infimum (greatest lower bound) of the range of $s$. This is defined as $\mathrm{sInf}(\mathrm{range}\, s)$.

infSet_to_nonempty instance

(α) [InfSet α] : Nonempty α

Full source

instance (priority := 50) infSet_to_nonempty (α) [InfSet α] : Nonempty α :=
  ⟨sInf ∅⟩

Nonemptiness of Types with Infimum Structure

Informal description

For any type $\alpha$ equipped with an infimum structure (i.e., a greatest lower bound operation for subsets), the type $\alpha$ is nonempty.

supSet_to_nonempty instance

(α) [SupSet α] : Nonempty α

Full source

instance (priority := 50) supSet_to_nonempty (α) [SupSet α] : Nonempty α :=
  ⟨sSup ∅⟩

Nonemptiness of Types with Supremum Structure

Informal description

For any type $\alpha$ equipped with a supremum structure (i.e., a least upper bound operation for subsets), the type $\alpha$ is nonempty.

term⨆_,_ definition

: Lean.ParserDescr✝

Full source

/-- Indexed supremum. -/
notation3 "⨆ "(...)", "r:60:(scoped f => iSup f) => r

Indexed supremum notation

Informal description

The notation `⨆ i, f i` represents the supremum of an indexed family of elements, where `f` is a function mapping indices to elements of a type with a supremum operation. This is equivalent to taking the supremum of the range of `f`.

term⨆_,_.delab_app.iSup definition

: Delab✝

Full source

/-- Indexed supremum. -/
notation3 "⨆ "(...)", "r:60:(scoped f => iSup f) => r

Indexed supremum notation

Informal description

The notation `⨆ i, f i` represents the indexed supremum of the family of elements `f i` over the index `i`. This is defined as the supremum of the set obtained by taking the range of the function `f`.

term⨅_,_ definition

: Lean.ParserDescr✝

Full source

/-- Indexed infimum. -/
notation3 "⨅ "(...)", "r:60:(scoped f => iInf f) => r

Indexed infimum notation

Informal description

The notation `⨅ i, f i` represents the indexed infimum of the family `f`, defined as the infimum of the range of `f`. This is equivalent to `sInf (Set.range f)`.

term⨅_,_.delab_app.iInf definition

: Delab✝

Full source

/-- Indexed infimum. -/
notation3 "⨅ "(...)", "r:60:(scoped f => iInf f) => r

Indexed infimum notation

Informal description

The notation `⨅ i, f i` represents the indexed infimum of the family `f`, which is defined as the infimum of the range of `f`.

iSup_delab definition

: Delab

Full source

/-- Delaborator for indexed supremum. -/
@[app_delab iSup]
def iSup_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
  let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
  unless f.isLambda do failure
  let prop ← Meta.isProp ι
  let dep := f.bindingBody!.hasLooseBVar 0
  let ppTypes ← getPPOption getPPFunBinderTypes
  let stx ← SubExpr.withAppArg do
    let dom ← SubExpr.withBindingDomain delab
    withBindingBodyUnusedName fun x => do
      let x : TSyntax `ident := .mk x
      let body ← delab
      if prop && !dep then
        `(⨆ (_ : $dom), $body)
      else if prop || ppTypes then
        `(⨆ ($x:ident : $dom), $body)
      else
        `(⨆ $x:ident, $body)
  -- Cute binders
  let stx : Term ←
    match stx with
    | `(⨆ $x:ident, ⨆ (_ : $y:ident ∈ $s), $body)
    | `(⨆ ($x:ident : $_), ⨆ (_ : $y:ident ∈ $s), $body) =>
      if x == y then `(⨆ $x:ident ∈ $s, $body) else pure stx
    | _ => pure stx
  return stx

Delaborator for indexed supremum notation

Informal description

The delaborator for indexed supremum notation `⨆` transforms Lean expressions into pretty-printed syntax. It handles different cases of binder notation (implicit vs explicit, with or without types) and optimizes nested binders of the form `⨆ x, ⨆ (x ∈ s), ...` into the more concise `⨆ x ∈ s, ...`.

iInf_delab definition

: Delab

Full source

/-- Delaborator for indexed infimum. -/
@[app_delab iInf]
def iInf_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
  let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
  unless f.isLambda do failure
  let prop ← Meta.isProp ι
  let dep := f.bindingBody!.hasLooseBVar 0
  let ppTypes ← getPPOption getPPFunBinderTypes
  let stx ← SubExpr.withAppArg do
    let dom ← SubExpr.withBindingDomain delab
    withBindingBodyUnusedName fun x => do
      let x : TSyntax `ident := .mk x
      let body ← delab
      if prop && !dep then
        `(⨅ (_ : $dom), $body)
      else if prop || ppTypes then
        `(⨅ ($x:ident : $dom), $body)
      else
        `(⨅ $x:ident, $body)
  -- Cute binders
  let stx : Term ←
    match stx with
    | `(⨅ $x:ident, ⨅ (_ : $y:ident ∈ $s), $body)
    | `(⨅ ($x:ident : $_), ⨅ (_ : $y:ident ∈ $s), $body) =>
      if x == y then `(⨅ $x:ident ∈ $s, $body) else pure stx
    | _ => pure stx
  return stx

Delaborator for indexed infimum notation

Informal description

The delaborator for indexed infimum notation `⨅`, which transforms Lean's internal representation of indexed infima into the mathematical notation `⨅ i, f i` or its variants depending on the context. It handles different cases including: - Simple binders (`⨅ x, f x`) - Typed binders (`⨅ (x : α), f x`) - Membership binders (`⨅ x ∈ s, f x`) - Propositional cases (`⨅ (_ : p), f`)

Set.instInfSet instance

: InfSet (Set α)

Full source

instance : InfSet (Set α) :=
  ⟨fun s => { a | ∀ t ∈ s, a ∈ t }⟩

Infimum Operator for Power Sets

Informal description

For any type $\alpha$, the power set $\mathcal{P}(\alpha)$ has an infimum operator where for any collection of sets $S \subseteq \mathcal{P}(\alpha)$, $\operatorname{sInf} S$ is the intersection of all sets in $S$.

Set.instSupSet instance

: SupSet (Set α)

Full source

instance : SupSet (Set α) :=
  ⟨fun s => { a | ∃ t ∈ s, a ∈ t }⟩

Supremum Operator for Power Sets

Informal description

For any type $\alpha$, the power set $\mathcal{P}(\alpha)$ has a supremum operator where for any collection of sets $S \subseteq \mathcal{P}(\alpha)$, $\operatorname{sSup} S$ is the union of all sets in $S$.

Set.sInter definition

(S : Set (Set α)) : Set α

Full source

/-- Intersection of a set of sets. -/
def sInter (S : Set (Set α)) : Set α :=
  sInf S

Intersection of a set of sets

Informal description

For a set $ S $ of subsets of a type $ \alpha $, the intersection $ \bigcap₀ S $ is the set of all elements of $ \alpha $ that belong to every set in $ S $. This is equivalent to taking the infimum of $ S $ in the power set of $ \alpha $.

Set.term⋂₀_ definition

: Lean.ParserDescr✝

Full source

/-- Notation for `Set.sInter` Intersection of a set of sets. -/
prefix:110 "⋂₀ " => sInter

Intersection of a set of sets (notation)

Informal description

The notation `⋂₀ S` denotes the intersection of a set of sets `S`, which is the set of all elements that belong to every set in `S`.

Set.sUnion definition

(S : Set (Set α)) : Set α

Full source

/-- Union of a set of sets. -/
def sUnion (S : Set (Set α)) : Set α :=
  sSup S

Union of a set of sets

Informal description

For a set $ S $ consisting of subsets of a type $ \alpha $, the union of all sets in $ S $ is denoted by $ \bigcup₀ S $. This is equivalent to taking the supremum of $ S $ in the lattice of subsets of $ \alpha $.

Set.term⋃₀_ definition

: Lean.ParserDescr✝

Full source

/-- Notation for `Set.sUnion`. Union of a set of sets. -/
prefix:110 "⋃₀ " => sUnion

Union of a set of sets

Informal description

The notation `⋃₀ S` represents the union of a set of sets `S`, which is the set of all elements that belong to at least one set in `S`.

Set.mem_sInter theorem

{x : α} {S : Set (Set α)} : x ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t

Full source

@[simp]
theorem mem_sInter {x : α} {S : Set (Set α)} : x ∈ ⋂₀ Sx ∈ ⋂₀ S ↔ ∀ t ∈ S, x ∈ t :=
  Iff.rfl

Characterization of Membership in Intersection of a Set of Sets

Informal description

For any element $x$ of type $\alpha$ and any collection $S$ of subsets of $\alpha$, the element $x$ belongs to the intersection $\bigcap₀ S$ if and only if for every set $t \in S$, $x$ belongs to $t$.

Set.mem_sUnion theorem

{x : α} {S : Set (Set α)} : x ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t

Full source

@[simp]
theorem mem_sUnion {x : α} {S : Set (Set α)} : x ∈ ⋃₀ Sx ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t :=
  Iff.rfl

Characterization of Membership in Union of a Set of Sets

Informal description

For any element $x$ of type $\alpha$ and any collection $S$ of subsets of $\alpha$, the element $x$ belongs to the union $\bigcup₀ S$ if and only if there exists a set $t \in S$ such that $x \in t$.

Set.iUnion definition

(s : ι → Set α) : Set α

Full source

/-- Indexed union of a family of sets -/
def iUnion (s : ι → Set α) : Set α :=
  iSup s

Indexed union of sets

Informal description

For an indexed family of sets $ s : \iota \to \text{Set } \alpha $, the term $ \bigcup_i s_i $ denotes the union of all sets in the family, i.e., the set of elements that belong to at least one set $ s_i $. This is defined as the supremum of the range of $ s $.

Set.iInter definition

(s : ι → Set α) : Set α

Full source

/-- Indexed intersection of a family of sets -/
def iInter (s : ι → Set α) : Set α :=
  iInf s

Indexed intersection of sets

Informal description

For an indexed family of sets $ s : \iota \to \text{Set } \alpha $, the term $ \bigcap_i s_i $ denotes the intersection of all sets in the family, i.e., the set of elements that belong to every set $ s_i $. This is defined as the infimum of the range of $ s $.

Set.term⋃_,_ definition

: Lean.ParserDescr✝

Full source

/-- Notation for `Set.iUnion`. Indexed union of a family of sets -/
notation3 "⋃ "(...)", "r:60:(scoped f => iUnion f) => r

Indexed union notation

Informal description

The notation `⋃ i, s i` represents the indexed union of a family of sets `s : ι → Set α`, which is the set of all elements that belong to at least one set in the family. This is equivalent to `Set.iUnion s`.

Set.term⋃_,_.delab_app.Set.iUnion definition

: Delab✝

Full source

/-- Notation for `Set.iUnion`. Indexed union of a family of sets -/
notation3 "⋃ "(...)", "r:60:(scoped f => iUnion f) => r

Indexed union notation

Informal description

The notation `⋃ i, s i` represents the indexed union of a family of sets, where `s` is a family of sets indexed by `i`. This is equivalent to `Set.iUnion s`.

Set.term⋂_,_ definition

: Lean.ParserDescr✝

Full source

/-- Notation for `Set.iInter`. Indexed intersection of a family of sets -/
notation3 "⋂ "(...)", "r:60:(scoped f => iInter f) => r

Indexed intersection notation

Informal description

The notation `⋂ i, s i` represents the indexed intersection of a family of sets, where `s i` is a set for each index `i`. This is equivalent to `Set.iInter s`, which computes the intersection of all sets in the range of `s`.

Set.term⋂_,_.delab_app.Set.iInter definition

: Delab✝

Full source

/-- Notation for `Set.iInter`. Indexed intersection of a family of sets -/
notation3 "⋂ "(...)", "r:60:(scoped f => iInter f) => r

Indexed intersection notation

Informal description

The notation `⋂ i, f i` represents the indexed intersection of a family of sets, where `f` is a function that maps each index `i` to a set. This is equivalent to `Set.iInter f`, which computes the intersection of all sets in the range of `f`.

Set.iUnion_delab definition

: Delab

Full source

/-- Delaborator for indexed unions. -/
@[app_delab Set.iUnion]
def iUnion_delab : Delab := whenPPOption Lean.getPPNotation do
  let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
  unless f.isLambda do failure
  let prop ← Meta.isProp ι
  let dep := f.bindingBody!.hasLooseBVar 0
  let ppTypes ← getPPOption getPPFunBinderTypes
  let stx ← SubExpr.withAppArg do
    let dom ← SubExpr.withBindingDomain delab
    withBindingBodyUnusedName fun x => do
      let x : TSyntax `ident := .mk x
      let body ← delab
      if prop && !dep then
        `(⋃ (_ : $dom), $body)
      else if prop || ppTypes then
        `(⋃ ($x:ident : $dom), $body)
      else
        `(⋃ $x:ident, $body)
  -- Cute binders
  let stx : Term ←
    match stx with
    | `(⋃ $x:ident, ⋃ (_ : $y:ident ∈ $s), $body)
    | `(⋃ ($x:ident : $_), ⋃ (_ : $y:ident ∈ $s), $body) =>
      if x == y then `(⋃ $x:ident ∈ $s, $body) else pure stx
    | _ => pure stx
  return stx

Delaborator for indexed union notation

Informal description

The delaborator for indexed unions transforms the formal representation of a union over an indexed family of sets into the mathematical notation `⋃ i, s i`, where `i` is the index variable and `s i` represents the set at index `i`. It handles various cases including: - Simple unions `⋃ i, s i` - Typed unions `⋃ (i : ι), s i` - Filtered unions `⋃ i ∈ t, s i`

Set.sInter_delab definition

: Delab

Full source

/-- Delaborator for indexed intersections. -/
@[app_delab Set.iInter]
def sInter_delab : Delab := whenPPOption Lean.getPPNotation do
  let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
  unless f.isLambda do failure
  let prop ← Meta.isProp ι
  let dep := f.bindingBody!.hasLooseBVar 0
  let ppTypes ← getPPOption getPPFunBinderTypes
  let stx ← SubExpr.withAppArg do
    let dom ← SubExpr.withBindingDomain delab
    withBindingBodyUnusedName fun x => do
      let x : TSyntax `ident := .mk x
      let body ← delab
      if prop && !dep then
        `(⋂ (_ : $dom), $body)
      else if prop || ppTypes then
        `(⋂ ($x:ident : $dom), $body)
      else
        `(⋂ $x:ident, $body)
  -- Cute binders
  let stx : Term ←
    match stx with
    | `(⋂ $x:ident, ⋂ (_ : $y:ident ∈ $s), $body)
    | `(⋂ ($x:ident : $_), ⋂ (_ : $y:ident ∈ $s), $body) =>
      if x == y then `(⋂ $x:ident ∈ $s, $body) else pure stx
    | _ => pure stx
  return stx

Delaborator for indexed intersections

Informal description

The delaborator for indexed intersections, which translates the formal representation of an indexed intersection into a more readable notation. Specifically, it converts expressions of the form `sInf (Set.range f)` into the notation `⋂ i, f i` for an indexed family of sets `f : ι → Set α`.

Set.mem_iUnion theorem

{x : α} {s : ι → Set α} : (x ∈ ⋃ i, s i) ↔ ∃ i, x ∈ s i

Full source

@[simp]
theorem mem_iUnion {x : α} {s : ι → Set α} : (x ∈ ⋃ i, s i) ↔ ∃ i, x ∈ s i :=
  ⟨fun ⟨_, ⟨⟨a, (t_eq : s a = _)⟩, (h : x ∈ _)⟩⟩ => ⟨a, t_eq.symm ▸ h⟩, fun ⟨a, h⟩ =>
    ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩

Characterization of Membership in Indexed Union: $x \in \bigcup_i s_i \leftrightarrow \exists i, x \in s_i$

Informal description

For any element $x$ of type $\alpha$ and any indexed family of sets $s : \iota \to \text{Set } \alpha$, the element $x$ belongs to the union $\bigcup_i s_i$ if and only if there exists an index $i$ such that $x \in s_i$.

Set.mem_iInter theorem

{x : α} {s : ι → Set α} : (x ∈ ⋂ i, s i) ↔ ∀ i, x ∈ s i

Full source

@[simp]
theorem mem_iInter {x : α} {s : ι → Set α} : (x ∈ ⋂ i, s i) ↔ ∀ i, x ∈ s i :=
  ⟨fun (h : ∀ a ∈ { a : Set α | ∃ i, s i = a }, x ∈ a) a => h (s a) ⟨a, rfl⟩,
    fun h _ ⟨a, (eq : s a = _)⟩ => eq ▸ h a⟩

Characterization of Membership in Indexed Intersection: $x \in \bigcap_i s_i \leftrightarrow \forall i, x \in s_i$

Informal description

For any element $x$ of type $\alpha$ and any indexed family of sets $s : \iota \to \text{Set } \alpha$, the element $x$ belongs to the intersection $\bigcap_i s_i$ if and only if $x$ belongs to every set $s_i$ in the family.

Set.sSup_eq_sUnion theorem

(S : Set (Set α)) : sSup S = ⋃₀ S

Full source

@[simp]
theorem sSup_eq_sUnion (S : Set (Set α)) : sSup S = ⋃₀S :=
  rfl

Supremum of a Set of Sets Equals Their Union

Informal description

For any collection of sets $S \subseteq \mathcal{P}(\alpha)$, the supremum of $S$ (denoted $\operatorname{sSup} S$) is equal to the union of all sets in $S$ (denoted $\bigcup₀ S$).

Set.sInf_eq_sInter theorem

(S : Set (Set α)) : sInf S = ⋂₀ S

Full source

@[simp]
theorem sInf_eq_sInter (S : Set (Set α)) : sInf S = ⋂₀ S :=
  rfl

Infimum of a Set of Sets Equals Their Intersection

Informal description

For any collection of sets $S \subseteq \mathcal{P}(\alpha)$, the infimum of $S$ (denoted $\operatorname{sInf} S$) is equal to the intersection of all sets in $S$ (denoted $\bigcap₀ S$).

Set.iSup_eq_iUnion theorem

(s : ι → Set α) : iSup s = iUnion s

Full source

@[simp]
theorem iSup_eq_iUnion (s : ι → Set α) : iSup s = iUnion s :=
  rfl

Supremum of Sets Equals Indexed Union

Informal description

For any indexed family of sets $s : \iota \to \mathcal{P}(\alpha)$, the supremum of the family (denoted $\bigsqcup_i s_i$) is equal to the union of all sets in the family (denoted $\bigcup_i s_i$).

Set.iInf_eq_iInter theorem

(s : ι → Set α) : iInf s = iInter s

Full source

@[simp]
theorem iInf_eq_iInter (s : ι → Set α) : iInf s = iInter s :=
  rfl

Infimum of Sets Equals Indexed Intersection

Informal description

For any indexed family of sets $s : \iota \to \mathcal{P}(\alpha)$, the infimum of the family (denoted $\bigsqcap_i s_i$) is equal to the intersection of all sets in the family (denoted $\bigcap_i s_i$).

Main definitions

Notation