# Documentation

Std.Data.Sum.Basic

# 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 Std.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.

instance Sum.instDecidableEqSum :
{α : Type u_1} → {β : Type u_2} → [inst : ] → [inst : ] → DecidableEq (α β)
instance Sum.instBEqSum :
{α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst : BEq β] → BEq (α β)
def Sum.isLeft {α : Type u_1} {β : Type u_2} :
α βBool

Check if a sum is inl.

Instances For
def Sum.isRight {α : Type u_1} {β : Type u_2} :
α βBool

Check if a sum is inr.

Instances For
def Sum.getLeft {α : Type u_1} {β : Type u_2} (ab : α β) :
α

Retrieve the contents from a sum known to be inl.

Instances For
def Sum.getRight {α : Type u_1} {β : Type u_2} (ab : α β) :
β

Retrieve the contents from a sum known to be inr.

Instances For
def Sum.getLeft? {α : Type u_1} {β : Type u_2} :
α β

Check if a sum is inl and if so, retrieve its contents.

Instances For
def Sum.getRight? {α : Type u_1} {β : Type u_2} :
α β

Check if a sum is inr and if so, retrieve its contents.

Instances For
@[simp]
theorem Sum.isLeft_inl {α : Type u_1} {β : Type u_2} {x : α} :
@[simp]
theorem Sum.isLeft_inr {α : Type u_1} {β : Type u_2} {x : β} :
@[simp]
theorem Sum.isRight_inl {α : Type u_1} {β : Type u_2} {x : α} :
@[simp]
theorem Sum.isRight_inr {α : Type u_1} {β : Type u_2} {x : β} :
@[simp]
theorem Sum.getLeft_inl {α : Type u_1} {β : Type u_2} {x : α} (h : ) :
Sum.getLeft () h = x
@[simp]
theorem Sum.getRight_inr {α : Type u_1} {β : Type u_2} {x : β} (h : ) :
@[simp]
theorem Sum.getLeft?_inl {α : Type u_1} {β : Type u_2} {x : α} :
= some x
@[simp]
theorem Sum.getLeft?_inr {α : Type u_1} {β : Type u_2} {x : β} :
= none
@[simp]
theorem Sum.getRight?_inl {α : Type u_1} {β : Type u_2} {x : α} :
= none
@[simp]
theorem Sum.getRight?_inr {α : Type u_1} {β : Type u_2} {x : β} :
= some x
def Sum.elim {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) :
α βγ

Define a function on α ⊕ β by giving separate definitions on α and β.

Instances For
@[simp]
theorem Sum.elim_inl {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : αγ) (g : βγ) (x : α) :
Sum.elim f g () = f x
@[simp]
theorem Sum.elim_inr {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : αγ) (g : βγ) (x : β) :
Sum.elim f g () = g x
def Sum.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : αα') (g : ββ') :
α βα' β'

Map α ⊕ β to α' ⊕ β' sending α to α' and β to β'.

Instances For
@[simp]
theorem Sum.map_inl {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : αα') (g : ββ') (x : α) :
Sum.map f g () = Sum.inl (f x)
@[simp]
theorem Sum.map_inr {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : αα') (g : ββ') (x : β) :
Sum.map f g () = Sum.inr (g x)
def Sum.swap {α : Type u_1} {β : Type u_2} :
α ββ α

Swap the factors of a sum type

Instances For
@[simp]
theorem Sum.swap_inl {α : Type u_1} {β : Type u_2} {x : α} :
@[simp]
theorem Sum.swap_inr {α : Type u_1} {β : Type u_2} {x : β} :
inductive Sum.LiftRel {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (r : αγProp) (s : βδProp) :
α βγ δProp
• inl: ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : αγProp} {s : βδProp} {a : α} {c : γ}, r a cSum.LiftRel r s () ()

inl a and inl c are related via LiftRel r s if a and c are related via r.

• inr: ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : αγProp} {s : βδProp} {b : β} {d : δ}, s b dSum.LiftRel r s () ()

inr b and inr d are related via LiftRel r s if b and d are related via s.

Lifts pointwise two relations between α and γ and between β and δ to a relation between α ⊕ β and γ ⊕ δ.

Instances For
@[simp]
theorem Sum.liftRel_inl_inl :
∀ {α : Type u_1} {γ : Type u_2} {r : αγProp} {β : Type u_3} {δ : Type u_4} {s : βδProp} {a : α} {c : γ}, Sum.LiftRel r s () () r a c
@[simp]
theorem Sum.not_liftRel_inl_inr :
∀ {α : Type u_1} {γ : Type u_2} {r : αγProp} {β : Type u_3} {δ : Type u_4} {s : βδProp} {a : α} {d : δ}, ¬Sum.LiftRel r s () ()
@[simp]
theorem Sum.not_liftRel_inr_inl :
∀ {α : Type u_1} {γ : Type u_2} {r : αγProp} {β : Type u_3} {δ : Type u_4} {s : βδProp} {b : β} {c : γ}, ¬Sum.LiftRel r s () ()
@[simp]
theorem Sum.liftRel_inr_inr :
∀ {α : Type u_1} {γ : Type u_2} {r : αγProp} {β : Type u_3} {δ : Type u_4} {s : βδProp} {b : β} {d : δ}, Sum.LiftRel r s () () s b d
instance Sum.instForAllSumSumDecidableLiftRel {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : αγProp} {s : βδProp} [(a : α) → (c : γ) → Decidable (r a c)] [(b : β) → (d : δ) → Decidable (s b d)] (ab : α β) (cd : γ δ) :
inductive Sum.Lex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :
α βα βProp
• inl: ∀ {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {a₁ a₂ : α}, r a₁ a₂Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂)

inl a₁ and inl a₂ are related via Lex r s if a₁ and a₂ are related via r.

• inr: ∀ {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {b₁ b₂ : β}, s b₁ b₂Sum.Lex r s (Sum.inr b₁) (Sum.inr b₂)

inr b₁ and inr b₂ are related via Lex r s if b₁ and b₂ are related via s.

• sep: ∀ {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (a : α) (b : β), Sum.Lex r s () ()

inl a and inr b are always related via Lex r s.

Lexicographic order for sum. Sort all the inl a before the inr b, otherwise use the respective order on α or β.

Instances For
@[simp]
theorem Sum.lex_inl_inl :
∀ {α : Type u_1} {r : ααProp} {β : Type u_2} {s : ββProp} {a₁ a₂ : α}, Sum.Lex r s (Sum.inl a₁) (Sum.inl a₂) r a₁ a₂
@[simp]
theorem Sum.lex_inr_inr :
∀ {α : Type u_1} {r : ααProp} {β : Type u_2} {s : ββProp} {b₁ b₂ : β}, Sum.Lex r s (Sum.inr b₁) (Sum.inr b₂) s b₁ b₂
@[simp]
theorem Sum.lex_inr_inl :
∀ {α : Type u_1} {r : ααProp} {β : Type u_2} {s : ββProp} {b : β} {a : α}, ¬Sum.Lex r s () ()
instance Sum.instDecidableRelSumLex :
{α : Type u_1} → {r : ααProp} → {α_1 : Type u_2} → {s : α_1α_1Prop} → [inst : ] → [inst : ] → DecidableRel (Sum.Lex r s)