inductive Std.PRange.BoundShape : Type

The shape of a range's upper or lower bound: open, closed or unbounded.

• open : BoundShape

  An open upper (or lower) bound of this shape requires elements of a range to be less than (or greater than) the bound, excluding the bound itself.

• closed : BoundShape

  A closed upper (or lower) bound of this shape requires elements of a range to be less than or equal (or greater than or equal) to the bound.

• unbounded : BoundShape

  This bound shape signifies the absence of a range bound, so that the range is unbounded in at least one direction.

structure Std.PRange.RangeShape : Type

The shape of a range, consisting of the shape of its upper and lower bounds.

• lower : BoundShape

  The shape of the range's lower bound.

• upper : BoundShape

  The shape of the range's upper bound.

@[reducible, inline]

abbrev Std.PRange.Bound (shape : BoundShape) (α : Type u) : Type u

An upper or lower bound in α of the given shape.

Equations

• Std.PRange.Bound Std.PRange.BoundShape.open α = α
• Std.PRange.Bound Std.PRange.BoundShape.closed α = α
• Std.PRange.Bound Std.PRange.BoundShape.unbounded α = PUnit

structure Std.PRange (shape : PRange.RangeShape) (α : Type u) : Type u

A range of elements of some type α. It is characterized by its upper and lower bounds, which may be inclusive, exclusive or absent.

• a...=b is the range of elements greater than or equal to a and less than or equal to b.
• a<...=b is the range of elements greater than a and less than or equal to b.
• a...b or a...<b is the range of elements greater than or equal to a and less than b.
• a<...b or a<...<b is the range of elements greater than a and less than b.
• *...=b is the range of elements less than or equal to b.
• *...b or *...<b is the range of elements less than b.
• a...* is the range of elements greater than or equal to a.
• a<...* is the range of elements greater than a.
• *...* contains all elements of α.

• lower : Bound shape.lower α

  The lower bound of the range.

• upper : Bound shape.upper α

  The upper bound of the range.

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Std.PRange.«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.PRange.

Equations

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

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

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

Equations

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

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

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

Equations

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

class Std.PRange.SupportsLowerBound (shape : BoundShape) (α : Type u) : Type u

This typeclass provides decidable lower bound checks of the given shape.

Instances are automatically provided in the following cases:

• shape is open and there is an LT α instance
• shape is closed and there is an LE α instance
• shape is .unbounded

• IsSatisfied : Bound shape α → α → Prop
• decidableSatisfiesLowerBound : DecidableRel IsSatisfied

instance Std.PRange.instSupportsLowerBoundUnbounded {α : Type u_1} : SupportsLowerBound BoundShape.unbounded α

Equations

• Std.PRange.instSupportsLowerBoundUnbounded = { IsSatisfied := fun (x : Std.PRange.Bound Std.PRange.BoundShape.unbounded α) (x : α) => True, decidableSatisfiesLowerBound := inferInstance }

class Std.PRange.SupportsUpperBound (shape : BoundShape) (α : Type u) : Type u

This typeclass provides decidable upper bound checks of the given shape.

Instances are automatically provided in the following cases:

• shape is open and there is an LT α instance
• shape is closed and there is an LE α instance
• shape is .unbounded

• IsSatisfied : Bound shape α → α → Prop
• decidableSatisfiesUpperBound : DecidableRel IsSatisfied

instance Std.PRange.instSupportsUpperBoundUnbounded {α : Type u_1} : SupportsUpperBound BoundShape.unbounded α

Equations

• Std.PRange.instSupportsUpperBoundUnbounded = { IsSatisfied := fun (x : Std.PRange.Bound Std.PRange.BoundShape.unbounded α) (x : α) => True, decidableSatisfiesUpperBound := inferInstance }

instance Std.PRange.instDecidableRelBoundIsSatisfied {shape : BoundShape} {α : Type u_1} [i : SupportsLowerBound shape α] : DecidableRel SupportsLowerBound.IsSatisfied

Equations

• Std.PRange.instDecidableRelBoundIsSatisfied = Std.PRange.SupportsLowerBound.decidableSatisfiesLowerBound

instance Std.PRange.instDecidableRelBoundIsSatisfied_1 {shape : BoundShape} {α : Type u_1} [i : SupportsUpperBound shape α] : DecidableRel SupportsUpperBound.IsSatisfied

Equations

• Std.PRange.instDecidableRelBoundIsSatisfied_1 = Std.PRange.SupportsUpperBound.decidableSatisfiesUpperBound

instance Std.PRange.instMembershipMkOfSupportsLowerBoundOfSupportsUpperBound {sl su : BoundShape} {α : Type u_1} [SupportsLowerBound sl α] [SupportsUpperBound su α] : Membership α (PRange { lower := sl, upper := su } α)

Equations

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

instance Std.PRange.instDecidableMemMk {sl su : BoundShape} {α : Type u_1} {a : α} [SupportsLowerBound sl α] [SupportsUpperBound su α] (r : PRange { lower := sl, upper := su } α) : Decidable (a ∈ r)

Equations

• r.instDecidableMemMk = inferInstanceAs (Decidable (Std.PRange.SupportsLowerBound.IsSatisfied r.lower a ∧ Std.PRange.SupportsUpperBound.IsSatisfied r.upper a))

class Std.PRange.HasFiniteRanges (shape : BoundShape) (α : Type u_1) [SupportsUpperBound shape α] : Prop

This typeclass ensures that ranges with the given shape of upper bounds are always finite. This is a prerequisite for many functions and instances, such as PRange.toList or ForIn'.

• mem_of_satisfiesUpperBound (u : Bound shape α) : ∃ (enumeration : List α), ∀ (a : α), SupportsUpperBound.IsSatisfied u a → a ∈ enumeration

class Std.PRange.BoundedUpwardEnumerable (lowerBoundShape : BoundShape) (α : Type u) : Type u

This typeclass will usually be used together with UpwardEnumerable α. It provides the starting point from which to enumerate all the values above the given lower bound.

Instances are automatically generated in the following cases:

• lowerBoundShape is .closed
• lowerBoundShape is .open and there is an UpwardEnumerable α instance
• lowerBoundShape is .unbounded and there is a Least? α instance

• init? : Bound lowerBoundShape α → Option α

class Std.PRange.LawfulUpwardEnumerableLowerBound (sl : BoundShape) (α : Type u_1) [UpwardEnumerable α] [SupportsLowerBound sl α] [BoundedUpwardEnumerable sl α] : Prop

This typeclass ensures that the lower bound predicate from SupportsLowerBound sl α can be characterized in terms of UpwardEnumerable α and BoundedUpwardEnumerable sl α.

• isSatisfied_iff (a : α) (l : Bound sl α) : SupportsLowerBound.IsSatisfied l a ↔ ∃ (init : α), BoundedUpwardEnumerable.init? l = some init ∧ UpwardEnumerable.LE init a

  An element a satisfies the lower bound l if and only if it is BoundedUpwardEnumerable.init? l or one of its transitive successors.

class Std.PRange.LawfulUpwardEnumerableUpperBound (su : BoundShape) (α : Type u_1) [UpwardEnumerable α] [SupportsUpperBound su α] : Prop

This typeclass ensures that if b is a transitive successor of a and b satisfies an upper bound of the given shape, then a also satisfies the upper bound.

• isSatisfied_of_le (u : Bound su α) (a b : α) : SupportsUpperBound.IsSatisfied u b → UpwardEnumerable.LE a b → SupportsUpperBound.IsSatisfied u a

  If b is a transitive successor of a and b satisfies a certain upper bound, then a also satisfies the upper bound.

theorem Std.PRange.LawfulUpwardEnumerableLowerBound.isSatisfied_of_le {sl : BoundShape} {α : Type u_1} [SupportsLowerBound sl α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [BoundedUpwardEnumerable sl α] [LawfulUpwardEnumerableLowerBound sl α] (l : Bound sl α) (a b : α) (ha : SupportsLowerBound.IsSatisfied l a) (hle : UpwardEnumerable.LE a b) : SupportsLowerBound.IsSatisfied l b

class Std.PRange.LawfulClosedUpperBound (α : Type w) [SupportsUpperBound BoundShape.closed α] [UpwardEnumerable α] : Prop

This typeclass ensures that SupportsUpperBound .closed α and UpwardEnumerable α instances are compatible.

• isSatisfied_iff_le (u : Bound BoundShape.closed α) (a : α) : SupportsUpperBound.IsSatisfied u a ↔ UpwardEnumerable.LE a u

  A closed upper bound is satisfied for a if and only if it is greater than or equal to a according to UpwardEnumerable.LE.

class Std.PRange.LawfulOpenUpperBound (α : Type w) [SupportsUpperBound BoundShape.open α] [UpwardEnumerable α] : Prop

This typeclass ensures that SupportsUpperBound .open α and UpwardEnumerable α instances are compatible.

• isSatisfied_iff_le (u : Bound BoundShape.open α) (a : α) : SupportsUpperBound.IsSatisfied u a ↔ UpwardEnumerable.LT a u

  An open upper bound is satisfied for a if and only if it is greater than to a according to UpwardEnumerable.LT.

class Std.PRange.LawfulUnboundedUpperBound (α : Type w) [SupportsUpperBound BoundShape.unbounded α] : Prop

This typeclass ensures that according to SupportsUpperBound .unbounded α, every element is in bounds.

• isSatisfied (u : Bound BoundShape.unbounded α) (a : α) : SupportsUpperBound.IsSatisfied u a

  An unbounded upper bound is satisfied for every element.

instance Std.PRange.instSupportsLowerBoundOpenOfDecidableLT {α : Type u_1} [LT α] [DecidableLT α] : SupportsLowerBound BoundShape.open α

Equations

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

instance Std.PRange.instSupportsUpperBoundOpenOfDecidableLT {α : Type u_1} [LT α] [DecidableLT α] : SupportsUpperBound BoundShape.open α

Equations

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

instance Std.PRange.instSupportsLowerBoundClosedOfDecidableLE {α : Type u_1} [LE α] [DecidableLE α] : SupportsLowerBound BoundShape.closed α

Equations

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

instance Std.PRange.instSupportsUpperBoundClosedOfDecidableLE {α : Type u_1} [LE α] [DecidableLE α] : SupportsUpperBound BoundShape.closed α

Equations

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

instance Std.PRange.instBoundedUpwardEnumerableUnboundedOfLeast? {α : Type u_1} [Least? α] : BoundedUpwardEnumerable BoundShape.unbounded α

Equations

• Std.PRange.instBoundedUpwardEnumerableUnboundedOfLeast? = { init? := fun (x : Std.PRange.Bound Std.PRange.BoundShape.unbounded α) => Std.PRange.Least?.least? }

instance Std.PRange.instBoundedUpwardEnumerableOpenOfUpwardEnumerable {α : Type u_1} [UpwardEnumerable α] : BoundedUpwardEnumerable BoundShape.open α

Equations

• Std.PRange.instBoundedUpwardEnumerableOpenOfUpwardEnumerable = { init? := fun (lower : Std.PRange.Bound Std.PRange.BoundShape.open α) => Std.PRange.UpwardEnumerable.succ? lower }

instance Std.PRange.instBoundedUpwardEnumerableClosed {α : Type u_1} : BoundedUpwardEnumerable BoundShape.closed α

Equations

• Std.PRange.instBoundedUpwardEnumerableClosed = { init? := fun (lower : Std.PRange.Bound Std.PRange.BoundShape.closed α) => some lower }

instance Std.PRange.instLawfulClosedUpperBoundOfLawfulUpwardEnumerableLE {α : Type u_1} [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] : LawfulClosedUpperBound α

instance Std.PRange.instLawfulOpenUpperBoundOfLawfulUpwardEnumerableLT {α : Type u_1} [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] : LawfulOpenUpperBound α

instance Std.PRange.instLawfulUnboundedUpperBoundOfUpwardEnumerable {α : Type u_1} [UpwardEnumerable α] : LawfulUnboundedUpperBound α

class Std.PRange.ClosedOpenIntersection (shape : RangeShape) (α : Type w) : Type w

This typeclass allows taking the intersection of ranges of the given shape and half-open ranges.

An element should be contained in the intersection if and only if it is contained in both ranges. This is encoded in LawfulClosedOpenIntersection.

• intersection : PRange shape α → PRange { lower := BoundShape.closed, upper := BoundShape.open } α → PRange { lower := BoundShape.closed, upper := BoundShape.open } α

class Std.PRange.LawfulClosedOpenIntersection (shape : RangeShape) (α : Type w) [ClosedOpenIntersection shape α] [SupportsLowerBound shape.lower α] [SupportsUpperBound shape.upper α] [SupportsLowerBound BoundShape.closed α] [SupportsUpperBound BoundShape.open α] : Prop

This typeclass ensures that the intersection according to ClosedOpenIntersection shape α of two ranges contains exactly those elements that are contained in both ranges.

• mem_intersection_iff {a : α} {r : PRange { lower := shape.lower, upper := shape.upper } α} {s : PRange { lower := BoundShape.closed, upper := BoundShape.open } α} : a ∈ ClosedOpenIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

  The intersection according to ClosedOpenIntersection shapee α of two ranges contains exactly those elements that are contained in both ranges.