# Documentation

Mathlib.Data.Sum.Basic

# Disjoint union of types #

This file proves basic results about the sum type α ⊕ β⊕ β.

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

## Main declarations #

• Sum.getLeft: Retrieves the left content of x : α ⊕ β⊕ β or returns none if it's coming from the right.
• Sum.getRight: Retrieves the right content of x : α ⊕ β⊕ β or returns none if it's coming from the left.
• 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.map: Maps α ⊕ β⊕ β to γ ⊕ δ⊕ δ component-wise.
• Sum.elim: Nondependent eliminator/induction principle for α ⊕ β⊕ β.
• Sum.swap: Maps α ⊕ β⊕ β to β ⊕ α⊕ α by swapping components.
• Sum.Lex: Lexicographic order on α ⊕ β⊕ β induced by a relation on α and a relation on β.

## 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 (α β)
Equations
• Sum.instDecidableEqSum = Sum.decEqSum✝
instance Sum.instBEqSum :
{α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst : BEq β] → BEq (α β)
Equations
• Sum.instBEqSum = { beq := Sum.beqSum✝ }
@[simp]
theorem Sum.forall {α : Type u} {β : Type v} {p : α βProp} :
((x : α β) → p x) ((a : α) → p ()) ((b : β) → p ())
@[simp]
theorem Sum.exists {α : Type u} {β : Type v} {p : α βProp} :
(x, p x) (a, p ()) b, p ()
theorem Sum.inl_injective {α : Type u} {β : Type v} :
theorem Sum.inr_injective {α : Type u} {β : Type v} :
def Sum.getLeft {α : Type u} {β : Type v} :
α β

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

Equations
def Sum.getRight {α : Type u} {β : Type v} :
α β

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

Equations
def Sum.isLeft {α : Type u} {β : Type v} :
α βBool

Check if a sum is inl.

Equations
def Sum.isRight {α : Type u} {β : Type v} :
α βBool

Check if a sum is inr.

Equations
@[simp]
theorem Sum.getLeft_inl {α : Type u} {β : Type v} (x : α) :
= some x
@[simp]
theorem Sum.getLeft_inr {α : Type u} {β : Type v} (x : β) :
= none
@[simp]
theorem Sum.getRight_inl {α : Type u} {β : Type v} (x : α) :
= none
@[simp]
theorem Sum.getRight_inr {α : Type u} {β : Type v} (x : β) :
= some x
@[simp]
theorem Sum.isLeft_inl {α : Type u} {β : Type v} (x : α) :
@[simp]
theorem Sum.isLeft_inr {α : Type u} {β : Type v} (x : β) :
@[simp]
theorem Sum.isRight_inl {α : Type u} {β : Type v} (x : α) :
@[simp]
theorem Sum.isRight_inr {α : Type u} {β : Type v} (x : β) :
@[simp]
theorem Sum.getLeft_eq_none_iff {α : Type u} {β : Type v} {x : α β} :
= none
@[simp]
theorem Sum.getRight_eq_none_iff {α : Type u} {β : Type v} {x : α β} :
= none
@[simp]
theorem Sum.getLeft_eq_some_iff {α : Type u} {β : Type v} {x : α β} {a : α} :
= some a x =
@[simp]
theorem Sum.getRight_eq_some_iff {α : Type u} {β : Type v} {x : α β} {b : β} :
x =
@[simp]
theorem Sum.not_isLeft {α : Type u} {β : Type v} (x : α β) :
() =
@[simp]
theorem Sum.isLeft_eq_false {α : Type u} {β : Type v} {x : α β} :
theorem Sum.Not_isLeft {α : Type u} {β : Type v} {x : α β} :
@[simp]
theorem Sum.not_isRight {α : Type u} {β : Type v} (x : α β) :
@[simp]
theorem Sum.isRight_eq_false {α : Type u} {β : Type v} {x : α β} :
theorem Sum.Not_isRight {α : Type u} {β : Type v} {x : α β} :
theorem Sum.isLeft_iff {α : Type u} {β : Type v} {x : α β} :
y, x =
theorem Sum.isRight_iff {α : Type u} {β : Type v} {x : α β} :
y, x =
theorem Sum.inl.inj_iff {α : Type u} {β : Type v} {a : α} {b : α} :
= a = b
theorem Sum.inr.inj_iff {α : Type u} {β : Type v} {a : β} {b : β} :
= a = b
theorem Sum.inl_ne_inr {α : Type u} {β : Type v} {a : α} {b : β} :
theorem Sum.inr_ne_inl {α : Type u} {β : Type v} {a : α} {b : β} :
def Sum.elim {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) :
α βγ

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

Equations
@[simp]
theorem Sum.elim_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) (x : α) :
Sum.elim f g () = f x
@[simp]
theorem Sum.elim_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) (x : β) :
Sum.elim f g () = g x
@[simp]
theorem Sum.elim_comp_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) :
Sum.elim f g Sum.inl = f
@[simp]
theorem Sum.elim_comp_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) :
Sum.elim f g Sum.inr = g
@[simp]
theorem Sum.elim_inl_inr {α : Type u_1} {β : Type u_2} :
Sum.elim Sum.inl Sum.inr = id
theorem Sum.comp_elim {α : Type u_1} {β : Type u_2} {γ : Sort u_3} {δ : Sort u_4} (f : γδ) (g : αγ) (h : βγ) :
f Sum.elim g h = Sum.elim (f g) (f h)
@[simp]
theorem Sum.elim_comp_inl_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α βγ) :
Sum.elim (f Sum.inl) (f Sum.inr) = f
def Sum.map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : αα') (g : ββ') :
α βα' β'

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

Equations
@[simp]
theorem Sum.map_inl {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : αα') (g : ββ') (x : α) :
Sum.map f g () = Sum.inl (f x)
@[simp]
theorem Sum.map_inr {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : αα') (g : ββ') (x : β) :
Sum.map f g () = Sum.inr (g x)
@[simp]
theorem Sum.map_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {α'' : Type u_1} {β'' : Type u_2} (f' : α'α'') (g' : β'β'') (f : αα') (g : ββ') (x : α β) :
Sum.map f' g' (Sum.map f g x) = Sum.map (f' f) (g' g) x
@[simp]
theorem Sum.map_comp_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {α'' : Type u_1} {β'' : Type u_2} (f' : α'α'') (g' : β'β'') (f : αα') (g : ββ') :
Sum.map f' g' Sum.map f g = Sum.map (f' f) (g' g)
@[simp]
theorem Sum.map_id_id (α : Type u_1) (β : Type u_2) :
Sum.map id id = id
theorem Sum.elim_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Sort u_5} {f₁ : αβ} {f₂ : βε} {g₁ : γδ} {g₂ : δε} {x : α γ} :
Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ f₁) (g₂ g₁) x
theorem Sum.elim_comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Sort u_5} {f₁ : αβ} {f₂ : βε} {g₁ : γδ} {g₂ : δε} :
Sum.elim f₂ g₂ Sum.map f₁ g₁ = Sum.elim (f₂ f₁) (g₂ g₁)
@[simp]
theorem Sum.isLeft_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : αβ) (g : γδ) (x : α γ) :
@[simp]
theorem Sum.isRight_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : αβ) (g : γδ) (x : α γ) :
@[simp]
theorem Sum.getLeft_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : αβ) (g : γδ) (x : α γ) :
@[simp]
theorem Sum.getRight_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : αβ) (g : γδ) (x : α γ) :
@[simp]
theorem Sum.update_elim_inl {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : DecidableEq (α β)] {f : αγ} {g : βγ} {i : α} {x : γ} :
@[simp]
theorem Sum.update_elim_inr {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : DecidableEq (α β)] {f : αγ} {g : βγ} {i : β} {x : γ} :
@[simp]
theorem Sum.update_inl_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : DecidableEq (α β)] {f : α βγ} {i : α} {x : γ} :
Function.update f () x Sum.inl = Function.update (f Sum.inl) i x
@[simp]
theorem Sum.update_inl_apply_inl {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : DecidableEq (α β)] {f : α βγ} {i : α} {j : α} {x : γ} :
Function.update f () x () = Function.update (f Sum.inl) i x j
@[simp]
theorem Sum.update_inl_comp_inr {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α β)] {f : α βγ} {i : α} {x : γ} :
Function.update f () x Sum.inr = f Sum.inr
theorem Sum.update_inl_apply_inr {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α β)] {f : α βγ} {i : α} {j : β} {x : γ} :
Function.update f () x () = f ()
@[simp]
theorem Sum.update_inr_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α β)] {f : α βγ} {i : β} {x : γ} :
Function.update f () x Sum.inl = f Sum.inl
theorem Sum.update_inr_apply_inl {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α β)] {f : α βγ} {i : α} {j : β} {x : γ} :
Function.update f () x () = f ()
@[simp]
theorem Sum.update_inr_comp_inr {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : DecidableEq (α β)] {f : α βγ} {i : β} {x : γ} :
Function.update f () x Sum.inr = Function.update (f Sum.inr) i x
@[simp]
theorem Sum.update_inr_apply_inr {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : DecidableEq (α β)] {f : α βγ} {i : β} {j : β} {x : γ} :
Function.update f () x () = Function.update (f Sum.inr) i x j
def Sum.swap {α : Type u} {β : Type v} :
α ββ α

Swap the factors of a sum type

Equations
@[simp]
theorem Sum.swap_inl {α : Type u} {β : Type v} (x : α) :
@[simp]
theorem Sum.swap_inr {α : Type u} {β : Type v} (x : β) :
@[simp]
theorem Sum.swap_swap {α : Type u} {β : Type v} (x : α β) :
Sum.swap () = x
@[simp]
theorem Sum.swap_swap_eq {α : Type u} {β : Type v} :
Sum.swap Sum.swap = id
@[simp]
theorem Sum.swap_leftInverse {α : Type u} {β : Type v} :
Function.LeftInverse Sum.swap Sum.swap
@[simp]
theorem Sum.swap_rightInverse {α : Type u} {β : Type v} :
Function.RightInverse Sum.swap Sum.swap
@[simp]
theorem Sum.isLeft_swap {α : Type u} {β : Type v} (x : α β) :
@[simp]
theorem Sum.isRight_swap {α : Type u} {β : Type v} (x : α β) :
@[simp]
theorem Sum.getLeft_swap {α : Type u} {β : Type v} (x : α β) :
@[simp]
theorem Sum.getRight_swap {α : Type u} {β : Type v} (x : α β) :
inductive Sum.LiftRel {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (r : αγProp) (s : βδProp) :
α βγ δProp

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

Instances For
@[simp]
theorem Sum.liftRel_inl_inl {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {a : α} {c : γ} :
Sum.LiftRel r s () () r a c
@[simp]
theorem Sum.not_liftRel_inl_inr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {a : α} {d : δ} :
¬Sum.LiftRel r s () ()
@[simp]
theorem Sum.not_liftRel_inr_inl {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {b : β} {c : γ} :
¬Sum.LiftRel r s () ()
@[simp]
theorem Sum.liftRel_inr_inr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {b : β} {d : δ} :
Sum.LiftRel r s () () s b d
instance Sum.instForAllSumSumDecidableLiftRel {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} [inst : (a : α) → (c : γ) → Decidable (r a c)] [inst : (b : β) → (d : δ) → Decidable (s b d)] (ab : α β) (cd : γ δ) :
Equations
• One or more equations did not get rendered due to their size.
theorem Sum.LiftRel.mono {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r₁ : αγProp} {r₂ : αγProp} {s₁ : βδProp} {s₂ : βδProp} {x : α β} {y : γ δ} (hr : (a : α) → (b : γ) → r₁ a br₂ a b) (hs : (a : β) → (b : δ) → s₁ a bs₂ a b) (h : Sum.LiftRel r₁ s₁ x y) :
Sum.LiftRel r₂ s₂ x y
theorem Sum.LiftRel.mono_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r₁ : αγProp} {r₂ : αγProp} {s : βδProp} {x : α β} {y : γ δ} (hr : (a : α) → (b : γ) → r₁ a br₂ a b) (h : Sum.LiftRel r₁ s x y) :
Sum.LiftRel r₂ s x y
theorem Sum.LiftRel.mono_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s₁ : βδProp} {s₂ : βδProp} {x : α β} {y : γ δ} (hs : (a : β) → (b : δ) → s₁ a bs₂ a b) (h : Sum.LiftRel r s₁ x y) :
Sum.LiftRel r s₂ x y
theorem Sum.LiftRel.swap {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} (h : Sum.LiftRel r s x y) :
Sum.LiftRel s r () ()
@[simp]
theorem Sum.liftRel_swap_iff {α : Type u} {β : Type v} {γ : Type u_2} {δ : Type u_1} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} :
Sum.LiftRel s r () () Sum.LiftRel r s x y
inductive Sum.Lex {α : Type u} {β : Type v} (r : ααProp) (s : ββProp) :
α βα βProp

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} {β : Type v} {r : ααProp} {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} {β : Type v} {r : ααProp} {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} {β : Type v} {r : ααProp} {s : ββProp} {a : α} {b : β} :
¬Sum.Lex r s () ()
instance Sum.instDecidableRelSumLex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
theorem Sum.LiftRel.lex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} {a : α β} {b : α β} (h : Sum.LiftRel r s a b) :
Sum.Lex r s a b
theorem Sum.liftRel_subrelation_lex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} :
theorem Sum.Lex.mono {α : Type u} {β : Type v} {r₁ : ααProp} {r₂ : ααProp} {s₁ : ββProp} {s₂ : ββProp} {x : α β} {y : α β} (hr : (a b : α) → r₁ a br₂ a b) (hs : (a b : β) → s₁ a bs₂ a b) (h : Sum.Lex r₁ s₁ x y) :
Sum.Lex r₂ s₂ x y
theorem Sum.Lex.mono_left {α : Type u} {β : Type v} {r₁ : ααProp} {r₂ : ααProp} {s : ββProp} {x : α β} {y : α β} (hr : (a b : α) → r₁ a br₂ a b) (h : Sum.Lex r₁ s x y) :
Sum.Lex r₂ s x y
theorem Sum.Lex.mono_right {α : Type u} {β : Type v} {r : ααProp} {s₁ : ββProp} {s₂ : ββProp} {x : α β} {y : α β} (hs : (a b : β) → s₁ a bs₂ a b) (h : Sum.Lex r s₁ x y) :
Sum.Lex r s₂ x y
theorem Sum.lex_acc_inl {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} {a : α} (aca : Acc r a) :
Acc (Sum.Lex r s) ()
theorem Sum.lex_acc_inr {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} (aca : ∀ (a : α), Acc (Sum.Lex r s) ()) {b : β} (acb : Acc s b) :
Acc (Sum.Lex r s) ()
theorem Sum.lex_wf {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} (ha : ) (hb : ) :
theorem Function.Injective.sum_elim {α : Type u} {β : Type v} {γ : Type u_1} {f : αγ} {g : βγ} (hf : ) (hg : ) (hfg : ∀ (a : α) (b : β), f a g b) :
theorem Function.Injective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : αβ} {g : α'β'} (hf : ) (hg : ) :
theorem Function.Surjective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : αβ} {g : α'β'} (hf : ) (hg : ) :
theorem Function.Bijective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : αβ} {g : α'β'} (hf : ) (hg : ) :
@[simp]
theorem Sum.map_injective {α : Type u} {β : Type v} {γ : Type u_2} {δ : Type u_1} {f : αγ} {g : βδ} :
@[simp]
theorem Sum.map_surjective {α : Type u} {β : Type v} {γ : Type u_2} {δ : Type u_1} {f : αγ} {g : βδ} :
@[simp]
theorem Sum.map_bijective {α : Type u} {β : Type v} {γ : Type u_2} {δ : Type u_1} {f : αγ} {g : βδ} :
theorem Sum.elim_const_const {α : Type u} {β : Type v} {γ : Type u_1} (c : γ) :
Sum.elim () () = Function.const (α β) c
@[simp]
theorem Sum.elim_lam_const_lam_const {α : Type u} {β : Type v} {γ : Type u_1} (c : γ) :
(Sum.elim (fun x => c) fun x => c) = fun x => c
theorem Sum.elim_update_left {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : ] (f : αγ) (g : βγ) (i : α) (c : γ) :
theorem Sum.elim_update_right {α : Type u} {β : Type v} {γ : Type u_1} [inst : ] [inst : ] (f : αγ) (g : βγ) (i : β) (c : γ) :

### Ternary sum #

Abbreviations for the maps from the summands to α ⊕ β ⊕ γ⊕ β ⊕ γ⊕ γ. This is useful for pattern-matching.

@[match_pattern]
def Sum3.in₀ {α : Type u} {β : Type v} {γ : Type u_1} (a : α) :
α β γ

The map from the first summand into a ternary sum.

Equations
@[match_pattern]
def Sum3.in₁ {α : Type u} {β : Type v} {γ : Type u_1} (b : β) :
α β γ

The map from the second summand into a ternary sum.

Equations
@[match_pattern]
def Sum3.in₂ {α : Type u} {β : Type v} {γ : Type u_1} (c : γ) :
α β γ

The map from the third summand into a ternary sum.

Equations