Init.Data.Sum.Basic

Module docstring

{"# Disjoint union of types

This file defines basic operations on the the sum type α ⊕ β.

α ⊕ β is the type made of a copy of α and a copy of β. It is also called disjoint union.

Main declarations

Sum.isLeft: Returns whether x : α ⊕ β comes from the left component or not.
Sum.isRight: Returns whether x : α ⊕ β comes from the right component or not.
Sum.getLeft: Retrieves the left content of a x : α ⊕ β that is known to come from the left.
Sum.getRight: Retrieves the right content of x : α ⊕ β that is known to come from the right.
Sum.getLeft?: Retrieves the left content of x : α ⊕ β as an option type or returns none if it's coming from the right.
Sum.getRight?: Retrieves the right content of x : α ⊕ β as an option type or returns none if it's coming from the left.
Sum.map: Maps α ⊕ β to γ ⊕ δ component-wise.
Sum.elim: Nondependent eliminator/induction principle for α ⊕ β.
Sum.swap: Maps α ⊕ β to β ⊕ α by swapping components.
Sum.LiftRel: The disjoint union of two relations.
Sum.Lex: Lexicographic order on α ⊕ β induced by a relation on α and a relation on β.

Further material

See Init.Data.Sum.Lemmas for theorems about these definitions.

Notes

The definition of Sum takes values in Type _. This effectively forbids Prop- valued sum types. To this effect, we have PSum, which takes value in Sort _ and carries a more complicated universe signature in consequence. The Prop version is Or. "}

Sum.instDecidableEq instance

{α✝} {β✝} [DecidableEq✝ α✝] [DecidableEq✝ β✝] : DecidableEq✝ (@Sum✝ α✝ β✝)

Full source

DecidableEq for Sum

Decidable Equality on Disjoint Union

Informal description

For any types $\alpha$ and $\beta$ with decidable equality, the disjoint union $\alpha \oplus \beta$ also has decidable equality. Specifically, given two elements $x, y \in \alpha \oplus \beta$, we can decide whether $x = y$ by checking if they are both in the left component and equal in $\alpha$, or both in the right component and equal in $\beta$.

Sum.instBEq instance

{α✝} {β✝} [BEq✝ α✝] [BEq✝ β✝] : BEq✝ (@Sum✝ α✝ β✝)

Full source

BEq for Sum

Boolean Equality on Disjoint Union

Informal description

For any types $\alpha$ and $\beta$ equipped with boolean equality relations, the disjoint union $\alpha \oplus \beta$ is also equipped with a boolean equality relation. This relation compares two elements of $\alpha \oplus \beta$ by first checking if they are both from $\alpha$ or both from $\beta$ (using the respective boolean equality relations), and returns `false` if they come from different components.

Sum.isLeft definition

: α ⊕ β → Bool

Full source

/-- Checks whether a sum is the left injection `inl`. -/
def isLeft : α ⊕ β → Bool
  | inl _ => true
  | inr _ => false

Check for left injection in disjoint union

Informal description

The function checks whether an element of the disjoint union $\alpha \oplus \beta$ is the left injection `inl`. It returns `true` if the element is of the form `inl _` and `false` otherwise.

Sum.isRight definition

: α ⊕ β → Bool

Full source

/-- Checks whether a sum is the right injection `inr`. -/
def isRight : α ⊕ β → Bool
  | inl _ => false
  | inr _ => true

Check for right injection in disjoint union

Informal description

The function checks whether an element of the disjoint union $\alpha \oplus \beta$ is the right injection `inr`. It returns `true` if the element is of the form `inr _` and `false` otherwise.

Sum.getLeft definition

: (ab : α ⊕ β) → ab.isLeft → α

Full source

/-- Retrieves the contents from a sum known to be `inl`.-/
def getLeft : (ab : α ⊕ β) → ab.isLeft → α
  | inl a, _ => a

Left component extraction from disjoint union

Informal description

Given an element $ab$ of the disjoint union $\alpha \oplus \beta$ and a proof that $ab$ is of the form $\text{inl}(a)$ (i.e., comes from the left component), this function returns the underlying element $a \in \alpha$.

Sum.getRight definition

: (ab : α ⊕ β) → ab.isRight → β

Full source

/-- Retrieves the contents from a sum known to be `inr`.-/
def getRight : (ab : α ⊕ β) → ab.isRight → β
  | inr b, _ => b

Right component extraction from disjoint union

Informal description

Given an element $ab$ of the disjoint union $\alpha \oplus \beta$ and a proof that $ab$ is of the form $\text{inr}(b)$ (i.e., comes from the right component), this function returns the underlying element $b \in \beta$.

Sum.getLeft? definition

: α ⊕ β → Option α

Full source

/-- Checks whether a sum is the left injection `inl` and, if so, retrieves its contents. -/
def getLeft? : α ⊕ β → Option α
  | inl a => some a
  | inr _ => none

Left component as optional value in a disjoint union

Informal description

Given an element of the disjoint union $\alpha \oplus \beta$, this function returns the left component as an optional value. Specifically, if the element is of the form $\text{inl}(a)$ for some $a \in \alpha$, it returns $\text{some}(a)$. If the element is of the form $\text{inr}(b)$ for some $b \in \beta$, it returns $\text{none}$.

Sum.getRight? definition

: α ⊕ β → Option β

Full source

/-- Checks whether a sum is the right injection `inr` and, if so, retrieves its contents. -/
def getRight? : α ⊕ β → Option β
  | inr b => some b
  | inl _ => none

Right component as optional value in a disjoint union

Informal description

Given an element of the disjoint union $\alpha \oplus \beta$, this function returns the right component as an optional value. Specifically, if the element is of the form $\text{inr}(b)$ for some $b \in \beta$, it returns $\text{some}(b)$. If the element is of the form $\text{inl}(a)$ for some $a \in \alpha$, it returns $\text{none}$.

Sum.isLeft_inl theorem

: (inl x : α ⊕ β).isLeft = true

Full source

@[simp] theorem isLeft_inl : (inl x : α ⊕ β).isLeft = true := rfl

Left Injection Yields True for `isLeft`

Informal description

For any element $x \in \alpha$, the function `isLeft` applied to the left injection $\text{inl}(x) \in \alpha \oplus \beta$ returns `true`.

Sum.isLeft_inr theorem

: (inr x : α ⊕ β).isLeft = false

Full source

@[simp] theorem isLeft_inr : (inr x : α ⊕ β).isLeft = false := rfl

Right Injection Yields False for `isLeft`

Informal description

For any element $x \in \beta$, the function `isLeft` applied to the right injection $\text{inr}(x) \in \alpha \oplus \beta$ returns `false$.

Sum.isRight_inl theorem

: (inl x : α ⊕ β).isRight = false

Full source

@[simp] theorem isRight_inl : (inl x : α ⊕ β).isRight = false := rfl

Left Injection Yields False for `isRight`

Informal description

For any element $x \in \alpha$, the function `isRight` applied to the left injection $\text{inl}(x) \in \alpha \oplus \beta$ returns `false`.

Sum.isRight_inr theorem

: (inr x : α ⊕ β).isRight = true

Full source

@[simp] theorem isRight_inr : (inr x : α ⊕ β).isRight = true := rfl

Right Injection Yields True for `isRight`

Informal description

For any element $x \in \beta$, the function `isRight` applied to the right injection $\text{inr}(x) \in \alpha \oplus \beta$ returns `true`.

Sum.getLeft_inl theorem

(h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x

Full source

@[simp] theorem getLeft_inl (h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x := rfl

Left Component Extraction from Left Injection Yields Original Element

Informal description

For any element $x \in \alpha$ and a proof $h$ that $\text{inl}(x) \in \alpha \oplus \beta$ is from the left component, the extraction of the left component from $\text{inl}(x)$ via $\text{getLeft}$ yields $x$, i.e., $\text{getLeft}(\text{inl}(x), h) = x$.

Sum.getRight_inr theorem

(h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x

Full source

@[simp] theorem getRight_inr (h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x := rfl

Right Component Extraction from Right Injection Yields Original Element

Informal description

For any element $x \in \beta$ and a proof $h$ that $\text{inr}(x) \in \alpha \oplus \beta$ is from the right component, the extraction of the right component from $\text{inr}(x)$ via $\text{getRight}$ yields $x$, i.e., $\text{getRight}(\text{inr}(x), h) = x$.

Sum.getLeft?_inl theorem

: (inl x : α ⊕ β).getLeft? = some x

Full source

@[simp] theorem getLeft?_inl : (inl x : α ⊕ β).getLeft? = some x := rfl

Left Component Extraction in Disjoint Union Yields Some for Left Input

Informal description

For any element $x$ in the left component of a disjoint union $\alpha \oplus \beta$, the function `getLeft?` applied to $\text{inl}(x)$ returns $\text{some}(x)$.

Sum.getLeft?_inr theorem

: (inr x : α ⊕ β).getLeft? = none

Full source

@[simp] theorem getLeft?_inr : (inr x : α ⊕ β).getLeft? = none := rfl

Left Component Extraction Yields None for Right Input in Disjoint Union

Informal description

For any element $x$ in the right component of a disjoint union $\alpha \oplus \beta$, the function `getLeft?` applied to $\text{inr}(x)$ returns `none`.

Sum.getRight?_inl theorem

: (inl x : α ⊕ β).getRight? = none

Full source

@[simp] theorem getRight?_inl : (inl x : α ⊕ β).getRight? = none := rfl

Right Component Extraction in Disjoint Union Yields None for Left Input

Informal description

For any element $x$ in the left component of a disjoint union $\alpha \oplus \beta$, the function `getRight?` applied to $\text{inl}(x)$ returns `none`.

Sum.getRight?_inr theorem

: (inr x : α ⊕ β).getRight? = some x

Full source

@[simp] theorem getRight?_inr : (inr x : α ⊕ β).getRight? = some x := rfl

Right Component Extraction in Disjoint Union Yields Some Value

Informal description

For any element $x$ in the right component of a disjoint union $\alpha \oplus \beta$, the function `getRight?` applied to $\text{inr}(x)$ returns $\text{some}(x)$.

Sum.elim definition

{α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ

Full source

/--
Case analysis for sums that applies the appropriate function `f` or `g` after checking which
constructor is present.
-/
protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
  fun x => Sum.casesOn x f g

Case analysis for disjoint unions

Informal description

Given functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, the function $\text{Sum.elim}\,f\,g \colon \alpha \oplus \beta \to \gamma$ applies $f$ to elements of $\alpha$ (tagged with $\text{inl}$) and $g$ to elements of $\beta$ (tagged with $\text{inr}$).

Sum.elim_inl theorem

(f : α → γ) (g : β → γ) (x : α) : Sum.elim f g (inl x) = f x

Full source

@[simp] theorem elim_inl (f : α → γ) (g : β → γ) (x : α) :
    Sum.elim f g (inl x) = f x := rfl

Case Analysis on Left Injection in Disjoint Union Yields Function Value

Informal description

For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, and any element $x \in \alpha$, applying the case analysis function $\text{Sum.elim}\,f\,g$ to the left injection $\text{inl}(x)$ yields $f(x)$.

Sum.elim_inr theorem

(f : α → γ) (g : β → γ) (x : β) : Sum.elim f g (inr x) = g x

Full source

@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
    Sum.elim f g (inr x) = g x := rfl

Elimination Rule for Right Injection in Disjoint Union

Informal description

For any functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$, and any element $x \in \beta$, the elimination function $\text{Sum.elim}\,f\,g$ applied to the right injection $\text{inr}\,x$ equals $g(x)$, i.e., \[ \text{Sum.elim}\,f\,g\,(\text{inr}\,x) = g(x). \]

Sum.map definition

(f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β'

Full source

/--
Transforms a sum according to functions on each type.

This function maps `α ⊕ β` to `α' ⊕ β'`, sending `α` to `α'` and `β` to `β'`.
-/
protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
  Sum.elim (inlinl ∘ f) (inrinr ∘ g)

Component-wise mapping of disjoint unions

Informal description

Given functions $f \colon \alpha \to \alpha'$ and $g \colon \beta \to \beta'$, the function $\text{Sum.map}\,f\,g \colon \alpha \oplus \beta \to \alpha' \oplus \beta'$ applies $f$ to elements of $\alpha$ (tagged with $\text{inl}$) and $g$ to elements of $\beta$ (tagged with $\text{inr}$), preserving the left/right structure of the sum type.

Sum.map_inl theorem

(f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x)

Full source

@[simp] theorem map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl

Mapping Preserves Left Injection in Disjoint Union

Informal description

For any functions $f \colon \alpha \to \alpha'$ and $g \colon \beta \to \beta'$, and any element $x \in \alpha$, the component-wise mapping of the disjoint union applied to the left injection $\text{inl}\,x$ satisfies: \[ \text{Sum.map}\,f\,g\,(\text{inl}\,x) = \text{inl}\,(f x). \]

Sum.map_inr theorem

(f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x)

Full source

@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl

Component-wise mapping preserves right injection: $\text{Sum.map}\,f\,g\,(\text{inr}\,x) = \text{inr}\,(g\,x)$

Informal description

For any functions $f \colon \alpha \to \alpha'$ and $g \colon \beta \to \beta'$, and any element $x \in \beta$, applying the component-wise mapping $\text{Sum.map}\,f\,g$ to the right injection $\text{inr}\,x$ yields $\text{inr}\,(g\,x)$.

Sum.swap definition

: α ⊕ β → β ⊕ α

Full source

/--
Swaps the factors of a sum type.

The constructor `Sum.inl` is replaced with `Sum.inr`, and vice versa.
-/
def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl

Swap of sum type components

Informal description

The function swaps the components of a sum type, mapping $\text{inl}\,x$ to $\text{inr}\,x$ and $\text{inr}\,y$ to $\text{inl}\,y$.

Sum.swap_inl theorem

: swap (inl x : α ⊕ β) = inr x

Full source

@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl

Swap of Left Injection in Disjoint Union

Informal description

For any element $x$ of type $\alpha$, the swap operation on the disjoint union $\alpha \oplus \beta$ maps the left injection $\text{inl}\,x$ to the right injection $\text{inr}\,x$.

Sum.swap_inr theorem

: swap (inr x : α ⊕ β) = inl x

Full source

@[simp] theorem swap_inr : swap (inr x : α ⊕ β) = inl x := rfl

Swap of Right Injection in Disjoint Union

Informal description

For any element $x$ of type $\beta$, the swap operation on the disjoint union $\alpha \oplus \beta$ maps the right injection $\text{inr}\,x$ to the left injection $\text{inl}\,x$ in $\beta \oplus \alpha$. That is, $\text{swap}(\text{inr}\,x) = \text{inl}\,x$.

Sum.LiftRel inductive

(r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop

Full source

/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
`α ⊕ β` and `γ ⊕ δ`. -/
inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
  /-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
  | protected inl {a c} : r a c → LiftRel r s (inl a) (inl c)
  /-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
  | protected inr {b d} : s b d → LiftRel r s (inr b) (inr d)

Lifted relation on disjoint unions

Informal description

Given relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$, the relation $\mathrm{LiftRel}\, r\, s$ on $\alpha \oplus \beta \to \gamma \oplus \delta \to \mathrm{Prop}$ is defined such that: - For $a \in \alpha$ and $c \in \gamma$, $\mathrm{LiftRel}\, r\, s\, (\mathrm{inl}\, a)\, (\mathrm{inl}\, c)$ holds if and only if $r\, a\, c$ holds. - For $b \in \beta$ and $d \in \delta$, $\mathrm{LiftRel}\, r\, s\, (\mathrm{inr}\, b)\, (\mathrm{inr}\, d)$ holds if and only if $s\, b\, d$ holds. - In all other cases (i.e., when comparing $\mathrm{inl}\, a$ with $\mathrm{inr}\, d$ or $\mathrm{inr}\, b$ with $\mathrm{inl}\, c$), $\mathrm{LiftRel}\, r\, s$ does not hold.

Sum.liftRel_inl_inl theorem

: LiftRel r s (inl a) (inl c) ↔ r a c

Full source

@[simp] theorem liftRel_inl_inl : LiftRelLiftRel r s (inl a) (inl c) ↔ r a c :=
  ⟨fun h => by cases h; assumption, LiftRel.inl⟩

Lifted Relation on Left Injections: $\mathrm{LiftRel}\, r\, s\, (\mathrm{inl}\, a)\, (\mathrm{inl}\, c) \leftrightarrow r\, a\, c$

Informal description

For any relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$, and any elements $a \in \alpha$ and $c \in \gamma$, the lifted relation $\mathrm{LiftRel}\, r\, s$ holds between $\mathrm{inl}\, a$ and $\mathrm{inl}\, c$ if and only if $r\, a\, c$ holds.

Sum.not_liftRel_inl_inr theorem

: ¬LiftRel r s (inl a) (inr d)

Full source

@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun

Non-relation between Left and Right Injections in Disjoint Union

Informal description

For any relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$, and any elements $a \in \alpha$ and $d \in \delta$, the lifted relation $\mathrm{LiftRel}\, r\, s$ does not hold between $\mathrm{inl}\, a$ (the left injection of $a$) and $\mathrm{inr}\, d$ (the right injection of $d$).

Sum.not_liftRel_inr_inl theorem

: ¬LiftRel r s (inr b) (inl c)

Full source

@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun

Non-relation between Right and Left Injections in Disjoint Union

Informal description

For any relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$, and any elements $b \in \beta$ and $c \in \gamma$, the lifted relation $\mathrm{LiftRel}\, r\, s$ does not hold between $\mathrm{inr}\, b$ (the right injection of $b$) and $\mathrm{inl}\, c$ (the left injection of $c$).

Sum.liftRel_inr_inr theorem

: LiftRel r s (inr b) (inr d) ↔ s b d

Full source

@[simp] theorem liftRel_inr_inr : LiftRelLiftRel r s (inr b) (inr d) ↔ s b d :=
  ⟨fun h => by cases h; assumption, LiftRel.inr⟩

Lifted Relation on Right Injections: $\mathrm{LiftRel}\, r\, s\, (\mathrm{inr}\, b)\, (\mathrm{inr}\, d) \leftrightarrow s\, b\, d$

Informal description

For any relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$, and any elements $b \in \beta$ and $d \in \delta$, the lifted relation $\mathrm{LiftRel}\, r\, s$ holds between $\mathrm{inr}\, b$ and $\mathrm{inr}\, d$ if and only if $s\, b\, d$ holds.

Sum.instDecidableLiftRel instance

 {r : α → γ → Prop} {s : β → δ → Prop} [∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
  ∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)

Full source

instance {r : α → γ → Prop} {s : β → δ → Prop}
    [∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
    ∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)
  | inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
  | inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
  | inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
  | inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr

Decidability of Lifted Relations on Disjoint Unions

Informal description

Given relations $r : \alpha \to \gamma \to \mathrm{Prop}$ and $s : \beta \to \delta \to \mathrm{Prop}$ such that $r(a, c)$ and $s(b, d)$ are decidable for all $a \in \alpha$, $c \in \gamma$, $b \in \beta$, and $d \in \delta$, then the lifted relation $\mathrm{LiftRel}\, r\, s$ on $\alpha \oplus \beta \to \gamma \oplus \delta \to \mathrm{Prop}$ is decidable. Specifically, for any $ab \in \alpha \oplus \beta$ and $cd \in \gamma \oplus \delta$, it is decidable whether $\mathrm{LiftRel}\, r\, s\, ab\, cd$ holds.

Sum.Lex inductive

(r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop

Full source

/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
respective order on `α` or `β`. -/
inductive Lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
  /-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
  | protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
  /-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
  | protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
  /-- `inl a` and `inr b` are always related via `Lex r s`. -/
  | sep (a b) : Lex r s (inl a) (inr b)

Lexicographic order on disjoint union

Informal description

The lexicographic order on the disjoint union $\alpha \oplus \beta$ induced by relations $r$ on $\alpha$ and $s$ on $\beta$. For any $x, y \in \alpha \oplus \beta$, the order is defined as follows: - If $x$ and $y$ are both from $\alpha$ (i.e., $x = \text{inl } a_1$ and $y = \text{inl } a_2$), then $x \leq y$ if and only if $r(a_1, a_2)$ holds. - If $x$ and $y$ are both from $\beta$ (i.e., $x = \text{inr } b_1$ and $y = \text{inr } b_2$), then $x \leq y$ if and only if $s(b_1, b_2)$ holds. - If $x$ is from $\alpha$ and $y$ is from $\beta$, then $x \leq y$ always holds. - If $x$ is from $\beta$ and $y$ is from $\alpha$, then $x \leq y$ does not hold.

Sum.lex_inl_inl theorem

: Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂

Full source

@[simp] theorem lex_inl_inl : LexLex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
  ⟨fun h => by cases h; assumption, Lex.inl⟩

Lexicographic Order on Left Injections Reflects Base Relation

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a_1, a_2 \in \alpha$, the lexicographic order $\text{Lex}(r, s)$ holds between $\text{inl}(a_1)$ and $\text{inl}(a_2)$ if and only if $r(a_1, a_2)$ holds.

Sum.lex_inr_inr theorem

: Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂

Full source

@[simp] theorem lex_inr_inr : LexLex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
  ⟨fun h => by cases h; assumption, Lex.inr⟩

Lexicographic Order on Right Injections Reflects Base Relation

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $b_1, b_2 \in \beta$, the lexicographic order $\text{Lex}(r, s)$ holds between $\text{inr}(b_1)$ and $\text{inr}(b_2)$ if and only if $s(b_1, b_2)$ holds.

Sum.lex_inr_inl theorem

: ¬Lex r s (inr b) (inl a)

Full source

@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun

Non-lexicographic ordering of right injection before left injection

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, and for any elements $a \in \alpha$ and $b \in \beta$, the lexicographic order $\text{Lex}(r, s)$ does not hold between $\text{inr}(b)$ and $\text{inl}(a)$. In other words, $\neg (\text{inr}(b) \leq_{\text{Lex}(r,s)} \text{inl}(a))$.

Sum.instDecidableRelSumLex instance

[DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)

Full source

instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
  | inl _, inl _ => decidable_of_iff' _ lex_inl_inl
  | inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
  | inr _, inl _ => Decidable.isFalse lex_inr_inl
  | inr _, inr _ => decidable_of_iff' _ lex_inr_inr

Decidability of Lexicographic Order on Disjoint Union

Informal description

For any decidable relations $r$ on $\alpha$ and $s$ on $\beta$, the lexicographic order $\text{Lex}(r, s)$ on the disjoint union $\alpha \oplus \beta$ is also decidable.