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 #

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 : DecidableEq α] → [inst : DecidableEq β] → 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 (Sum.inl a)) ((b : β) → p (Sum.inr b))
@[simp]
theorem Sum.exists {α : Type u} {β : Type v} {p : α βProp} :
(x, p x) (a, p (Sum.inl a)) b, p (Sum.inr b)
theorem Sum.inl_injective {α : Type u} {β : Type v} :
theorem Sum.inr_injective {α : Type u} {β : Type v} :
def Sum.getLeft {α : Type u} {β : Type v} :
α βOption α

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

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

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 : α) :
@[simp]
theorem Sum.getLeft_inr {α : Type u} {β : Type v} (x : β) :
@[simp]
theorem Sum.getRight_inl {α : Type u} {β : Type v} (x : α) :
@[simp]
theorem Sum.getRight_inr {α : Type u} {β : Type v} (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 : α β} :
@[simp]
theorem Sum.getRight_eq_none_iff {α : Type u} {β : Type v} {x : α β} :
@[simp]
theorem Sum.getLeft_eq_some_iff {α : Type u} {β : Type v} {x : α β} {a : α} :
@[simp]
theorem Sum.getRight_eq_some_iff {α : Type u} {β : Type v} {x : α β} {b : β} :
@[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 : α β} :
Sum.isLeft x = true y, x = Sum.inl y
theorem Sum.isRight_iff {α : Type u} {β : Type v} {x : α β} :
Sum.isRight x = true y, x = Sum.inr y
theorem Sum.inl.inj_iff {α : Type u} {β : Type v} {a : α} {b : α} :
theorem Sum.inr.inj_iff {α : Type u} {β : Type v} {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 (Sum.inl x) = f x
@[simp]
theorem Sum.elim_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) (x : β) :
Sum.elim f g (Sum.inr x) = 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 x) = 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 x) = 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 : DecidableEq α] [inst : DecidableEq (α β)] {f : αγ} {g : βγ} {i : α} {x : γ} :
@[simp]
theorem Sum.update_elim_inr {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst : DecidableEq (α β)] {f : αγ} {g : βγ} {i : β} {x : γ} :
@[simp]
theorem Sum.update_inl_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst : DecidableEq (α β)] {f : α βγ} {i : α} {x : γ} :
Function.update f (Sum.inl i) 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 : DecidableEq α] [inst : DecidableEq (α β)] {f : α βγ} {i : α} {j : α} {x : γ} :
Function.update f (Sum.inl i) x (Sum.inl j) = 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 (Sum.inl i) 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 : γ} :
@[simp]
theorem Sum.update_inr_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α β)] {f : α βγ} {i : β} {x : γ} :
Function.update f (Sum.inr i) 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 : γ} :
@[simp]
theorem Sum.update_inr_comp_inr {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq β] [inst : DecidableEq (α β)] {f : α βγ} {i : β} {x : γ} :
Function.update f (Sum.inr i) 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 : DecidableEq β] [inst : DecidableEq (α β)] {f : α βγ} {i : β} {j : β} {x : γ} :
Function.update f (Sum.inr i) x (Sum.inr j) = 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 : α β) :
@[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 (Sum.inl a) (Sum.inl c) 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 : δ} :
    @[simp]
    theorem Sum.not_liftRel_inr_inl {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {b : β} {c : γ} :
    @[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 (Sum.inr b) (Sum.inr d) 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) :
    @[simp]
    theorem Sum.liftRel_swap_iff {α : Type u} {β : Type v} {γ : Type u_2} {δ : Type u_1} {r : αγProp} {s : βδProp} {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 : β} :
      instance Sum.instDecidableRelSumLex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [inst : DecidableRel r] [inst : DecidableRel s] :
      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) (Sum.inl a)
      theorem Sum.lex_acc_inr {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} (aca : ∀ (a : α), Acc (Sum.Lex r s) (Sum.inl a)) {b : β} (acb : Acc s b) :
      Acc (Sum.Lex r s) (Sum.inr b)
      theorem Sum.lex_wf {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
      theorem Function.Injective.sum_elim {α : Type u} {β : Type v} {γ : Type u_1} {f : αγ} {g : βγ} (hf : Function.Injective f) (hg : Function.Injective g) (hfg : ∀ (a : α) (b : β), f a g b) :
      theorem Function.Injective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : αβ} {g : α'β'} (hf : Function.Injective f) (hg : Function.Injective g) :
      theorem Function.Surjective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : αβ} {g : α'β'} (hf : Function.Surjective f) (hg : Function.Surjective g) :
      theorem Function.Bijective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : αβ} {g : α'β'} (hf : Function.Bijective f) (hg : Function.Bijective g) :
      @[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 : γ) :
      @[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 : DecidableEq α] [inst : DecidableEq β] (f : αγ) (g : βγ) (i : α) (c : γ) :
      theorem Sum.elim_update_right {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq α] [inst : DecidableEq β] (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