structure Std.Rcc (α : Type u) : Type u

A range of elements of α with closed lower and upper bounds.

a...=b is the range of all values greater than or equal to a : α and less than or equal to b : α. This is notation for Rcc.mk a b.

• lower : α

  The lower bound of the range. lower is included in the range.

• upper : α

  The upper bound of the range. upper is included in the range.

structure Std.Rco (α : Type u) : Type u

A range of elements of α with a closed lower bound and an open upper bound.

a...b or a...<b is the range of all values greater than or equal to a : α and less than b : α. This is notation for Rco.mk a b.

• lower : α

  The lower bound of the range. lower is included in the range.

• upper : α

  The upper bound of the range. upper is not included in the range.

structure Std.Rci (α : Type u) : Type u

An upward-unbounded range of elements of α with a closed lower bound.

a...* is the range of all values greater than or equal to a : α. This is notation for Rci.mk a.

• lower : α

  The lower bound of the range. lower is included in the range.

structure Std.Roc (α : Type u) : Type u

A range of elements of α with an open lower bound and a closed upper bound.

a<...=b is the range of all values greater than a : α and less than or equal to b : α. This is notation for Roc.mk a b.

• lower : α

  The lower bound of the range. lower is not included in the range.

• upper : α

  The upper bound of the range. upper is included in the range.

structure Std.Roo (α : Type u) : Type u

A range of elements of α with an open lower and upper bounds.

a<...b or a<...<b is the range of all values greater than a : α and less than b : α. This is notation for Roo.mk a b.

• lower : α

  The lower bound of the range. lower is not included in the range.

• upper : α

  The upper bound of the range. upper is not included in the range.

structure Std.Roi (α : Type u) : Type u

An upward-unbounded range of elements of α with an open lower bound.

a<...* is the range of all values greater than a : α. This is notation for Roi.mk a.

• lower : α

  The lower bound of the range. lower is not included in the range.

structure Std.Ric (α : Type u) : Type u

A downward-unbounded range of elements of α with a closed upper bound.

*...=b is the range of all values less than or equal to b : α. This is notation for Ric.mk b.

• upper : α

  The upper bound of the range. upper is included in the range.

structure Std.Rio (α : Type u) : Type u

A downward-unbounded range of elements of α with an open upper bound.

*...b or *...<b is the range of all values less than b : α. This is notation for Rio.mk b.

• upper : α

  The upper bound of the range. upper is not included in the range.

structure Std.Rii (α : Type u) : Type

A full range of all elements of α. Its only inhabitant is the range *...*, which is notation for Rii.mk.

def Std.«term_...*» : Lean.TrailingParserDescr

a...* is the range of elements greater than or equal to a. See also Std.Rci.

Equations

• Std.«term_...*» = Lean.ParserDescr.trailingNode `Std.«term_...*» 1024 0 (Lean.ParserDescr.symbol "...*")

def Std.«term*...*» : Lean.ParserDescr

*...* is the range that is unbounded in both directions. See also Std.Rii.

Equations

• Std.«term*...*» = Lean.ParserDescr.node `Std.«term*...*» 1024 (Lean.ParserDescr.symbol "*...*")

def Std.«term_<...*» : Lean.TrailingParserDescr

a<...* is the range of elements greater than a. See also Std.Roi.

Equations

• Std.«term_<...*» = Lean.ParserDescr.trailingNode `Std.«term_<...*» 1024 0 (Lean.ParserDescr.symbol "<...*")

def Std.«term_...<_» : Lean.TrailingParserDescr

a...<b is the range of elements greater than or equal to a and less than b. See also Std.Rco.

Equations

• Std.«term_...<_» = Lean.ParserDescr.trailingNode `Std.«term_...<_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "...<") (Lean.ParserDescr.cat `term 0))

def Std.«term_..._» : Lean.TrailingParserDescr

a...b is the range of elements greater than or equal to a and less than b. See also Std.Rco.

Equations

• Std.«term_..._» = Lean.ParserDescr.trailingNode `Std.«term_..._» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "...") (Lean.ParserDescr.cat `term 0))

def Std.«term*...<_» : Lean.ParserDescr

*...<b is the range of elements less than b. See also Std.Rio.

Equations

• Std.«term*...<_» = Lean.ParserDescr.node `Std.«term*...<_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*...<") (Lean.ParserDescr.cat `term 0))

def Std.«term*..._» : Lean.ParserDescr

*...b is the range of elements less than b. See also Std.Rio.

Equations

• Std.«term*..._» = Lean.ParserDescr.node `Std.«term*..._» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*...") (Lean.ParserDescr.cat `term 0))

def Std.«term_<...<_» : Lean.TrailingParserDescr

a<...<b is the range of elements greater than a and less than b. See also Std.Roo.

Equations

• Std.«term_<...<_» = Lean.ParserDescr.trailingNode `Std.«term_<...<_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "<...<") (Lean.ParserDescr.cat `term 0))

def Std.«term_<..._» : Lean.TrailingParserDescr

a<...b is the range of elements greater than a and less than b. See also Std.Roo.

Equations

• Std.«term_<..._» = Lean.ParserDescr.trailingNode `Std.«term_<..._» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "<...") (Lean.ParserDescr.cat `term 0))

def Std.«term_...=_» : Lean.TrailingParserDescr

a...=b is the range of elements greater than or equal to a and less than or equal to b. See also Std.Rcc.

Equations

• Std.«term_...=_» = Lean.ParserDescr.trailingNode `Std.«term_...=_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "...=") (Lean.ParserDescr.cat `term 0))

def Std.«term*...=_» : Lean.ParserDescr

*...=b is the range of elements less than or equal to b. See also Std.Ric.

Equations

• Std.«term*...=_» = Lean.ParserDescr.node `Std.«term*...=_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*...=") (Lean.ParserDescr.cat `term 0))

def Std.«term_<...=_» : Lean.TrailingParserDescr

a<...=b is the range of elements greater than a and less than or equal to b. See also Std.Roc.

Equations

• Std.«term_<...=_» = Lean.ParserDescr.trailingNode `Std.«term_<...=_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "<...=") (Lean.ParserDescr.cat `term 0))

class Std.Rxc.IsAlwaysFinite (α : Type u) [PRange.UpwardEnumerable α] [LE α] : Prop

This type class ensures that right-closed ranges (i.e., for bounds a and b, a...=b, a<...=b and *...=b) are always finite. This is a prerequisite for many functions and instances, such as Rcc.toList or ForIn'.

• finite (init hi : α) : ∃ (n : Nat), (PRange.succMany? n init).elim True fun (x : α) => ¬x ≤ hi

  For every pair of elements init and hi, there exists a chain of successors that results in an element that either has no successors or is greater than hi.

class Std.Rxo.IsAlwaysFinite (α : Type u) [PRange.UpwardEnumerable α] [LT α] : Prop

This type class ensures that right-open ranges (i.e., for bounds a and b, a...b, a<...b and *...b) are always finite. This is a prerequisite for many functions and instances, such as Rco.toList or ForIn'.

• finite (init hi : α) : ∃ (n : Nat), (PRange.succMany? n init).elim True fun (x : α) => ¬x < hi

  For every pair of elements init and hi, there exists a chain of successors that results in an element that either has no successors or is greater than hi.

class Std.Rxi.IsAlwaysFinite (α : Type u) [PRange.UpwardEnumerable α] : Prop

This type class ensures that right-unbounded ranges (i.e., for a bound a, a...*, a<...* and *...*) are always finite. This is a prerequisite for many functions and instances, such as Rci.toList or ForIn'.

• finite (init : α) : ∃ (n : Nat), PRange.succMany? n init = none

  For every elements init, there exists a chain of successors that results in an element that has no successors.

instance Std.Rcc.instMembershipOfLE {α : Type u} [LE α] : Membership α (Rcc α)

Equations

• Std.Rcc.instMembershipOfLE = { mem := fun (r : Std.Rcc α) (a : α) => r.lower ≤ a ∧ a ≤ r.upper }

instance Std.Rcc.instDecidableMemOfDecidableLE {α : Type u} {r : Rcc α} {a : α} [LE α] [DecidableLE α] : Decidable (a ∈ r)

Equations

• Std.Rcc.instDecidableMemOfDecidableLE = inferInstanceAs (Decidable (r.lower ≤ a ∧ a ≤ r.upper))

instance Std.Rco.instMembershipOfLEOfLT {α : Type u} [LE α] [LT α] : Membership α (Rco α)

Equations

• Std.Rco.instMembershipOfLEOfLT = { mem := fun (r : Std.Rco α) (a : α) => r.lower ≤ a ∧ a < r.upper }

instance Std.Rco.instDecidableMemOfDecidableLEOfDecidableLT {α : Type u} {r : Rco α} {a : α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] : Decidable (a ∈ r)

Equations

• Std.Rco.instDecidableMemOfDecidableLEOfDecidableLT = inferInstanceAs (Decidable (r.lower ≤ a ∧ a < r.upper))

instance Std.Rci.instMembershipOfLE {α : Type u} [LE α] : Membership α (Rci α)

Equations

• Std.Rci.instMembershipOfLE = { mem := fun (r : Std.Rci α) (a : α) => r.lower ≤ a }

instance Std.Rci.instDecidableMemOfDecidableLE {α : Type u} {r : Rci α} {a : α} [LE α] [DecidableLE α] : Decidable (a ∈ r)

Equations

• Std.Rci.instDecidableMemOfDecidableLE = inferInstanceAs (Decidable (r.lower ≤ a))

instance Std.Roc.instMembershipOfLEOfLT {α : Type u} [LE α] [LT α] : Membership α (Roc α)

Equations

• Std.Roc.instMembershipOfLEOfLT = { mem := fun (r : Std.Roc α) (a : α) => r.lower < a ∧ a ≤ r.upper }

instance Std.Roc.instDecidableMemOfDecidableLEOfDecidableLT {α : Type u} {r : Roc α} {a : α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] : Decidable (a ∈ r)

Equations

• Std.Roc.instDecidableMemOfDecidableLEOfDecidableLT = inferInstanceAs (Decidable (r.lower < a ∧ a ≤ r.upper))

instance Std.Roo.instMembershipOfLT {α : Type u} [LT α] : Membership α (Roo α)

Equations

• Std.Roo.instMembershipOfLT = { mem := fun (r : Std.Roo α) (a : α) => r.lower < a ∧ a < r.upper }

instance Std.Roo.instDecidableMemOfDecidableLT {α : Type u} {r : Roo α} {a : α} [LT α] [DecidableLT α] : Decidable (a ∈ r)

Equations

• Std.Roo.instDecidableMemOfDecidableLT = inferInstanceAs (Decidable (r.lower < a ∧ a < r.upper))

instance Std.Roi.instMembershipOfLT {α : Type u} [LT α] : Membership α (Roi α)

Equations

• Std.Roi.instMembershipOfLT = { mem := fun (r : Std.Roi α) (a : α) => r.lower < a }

instance Std.Roi.instDecidableMemOfDecidableLT {α : Type u} {r : Roi α} {a : α} [LT α] [DecidableLT α] : Decidable (a ∈ r)

Equations

• Std.Roi.instDecidableMemOfDecidableLT = inferInstanceAs (Decidable (r.lower < a))

instance Std.Ric.instMembershipOfLE {α : Type u} [LE α] : Membership α (Ric α)

Equations

• Std.Ric.instMembershipOfLE = { mem := fun (r : Std.Ric α) (a : α) => a ≤ r.upper }

instance Std.Ric.instDecidableMemOfDecidableLE {α : Type u} {r : Ric α} {a : α} [LE α] [DecidableLE α] : Decidable (a ∈ r)

Equations

• Std.Ric.instDecidableMemOfDecidableLE = inferInstanceAs (Decidable (a ≤ r.upper))

instance Std.Rio.instMembershipOfLT {α : Type u} [LT α] : Membership α (Rio α)

Equations

• Std.Rio.instMembershipOfLT = { mem := fun (r : Std.Rio α) (a : α) => a < r.upper }

instance Std.Rio.instDecidableMemOfDecidableLT {α : Type u} {r : Rio α} {a : α} [LT α] [DecidableLT α] : Decidable (a ∈ r)

Equations

• Std.Rio.instDecidableMemOfDecidableLT = inferInstanceAs (Decidable (a < r.upper))

instance Std.Rii.instMembership {α : Type u} : Membership α (Rii α)

Equations

• Std.Rii.instMembership = { mem := fun (x : Std.Rii α) (x_1 : α) => True }

instance Std.Rii.instDecidableMem {α : Type u} {r : Rii α} {a : α} : Decidable (a ∈ r)

Equations

• Std.Rii.instDecidableMem = inferInstanceAs (Decidable True)

class Std.Rcc.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of a closed range with a left-closed right-open range, resulting in another left-closed right-open range.

• intersection : Rcc α → Rco α → Rco α

  The intersection operator.

class Std.Rcc.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Rcc.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : Rcc α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.

class Std.Rco.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of two left-closed right-open ranges, resulting in another left-closed right-open range.

• intersection : Rco α → Rco α → Rco α

  The intersection operator.

class Std.Rco.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Rco.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.

class Std.Rci.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of a left-closed right-unbounded range with a left-closed right-open range, resulting in another left-closed right-open range.

• intersection : Rci α → Rco α → Rco α

  The intersection operator.

class Std.Rci.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Rci.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : Rci α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.

class Std.Roc.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of a left-open right-closed range with a left-closed right-open range, resulting in another left-closed right-open range.

• intersection : Roc α → Rco α → Rco α

  The intersection operator.

class Std.Roc.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Roc.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : Roc α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.

class Std.Roo.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of an open range with a left-closed right-open range, resulting in another left-closed right-open range.

• intersection : Roo α → Rco α → Rco α

  The intersection operator.

class Std.Roo.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Roo.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : Roo α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.

class Std.Roi.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of a left-open right-unbounded range with a left-closed right-open range, resulting in another left-closed right-open range.

• intersection : Roi α → Rco α → Rco α

  The intersection operator.

class Std.Roi.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Roi.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : Roi α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.

class Std.Ric.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of a left-unbounded right-closed range with a left-closed right-open range, resulting in another left-closed right-open range.

• intersection : Ric α → Rco α → Rco α

  The intersection operator.

class Std.Ric.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Ric.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : Ric α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.

class Std.Rio.HasRcoIntersection (α : Type w) : Type w

This type class allows taking the intersection of a left-unbounded right-open range with a left-closed right-open range, resulting in another left-closed right-open range.

• intersection : Rio α → Rco α → Rco α

  The intersection operator.

class Std.Rio.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] : Prop

This type class ensures that the intersection according to Rio.HasRcoIntersection of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : Rio α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  Every element of the intersection is an element of both original ranges.