mathlib3 documentation

data.sum.basic

Disjoint union of types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.get_left: Retrieves the left content of x : α ⊕ β or returns none if it's coming from the right.
sum.get_right: Retrieves the right content of x : α ⊕ β or returns none if it's coming from the left.
sum.is_left: Returns whether x : α ⊕ β comes from the left component or not.
sum.is_right: 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.

@[protected, instance]

def sum.decidable_eq (α : Type u) [a : decidable_eq α] (β : Type v) [a_1 : decidable_eq β] :

decidable_eq (α ⊕ β)

@[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} :

function.injective sum.inl

theorem sum.inr_injective {α : Type u} {β : Type v} :

function.injective sum.inr

@[simp]

def sum.get_left {α : Type u} {β : Type v} :

α ⊕ β → option α

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

Equations

(sum.inr _x).get_left = option.none
(sum.inl a).get_left = option.some a

@[simp]

def sum.get_right {α : Type u} {β : Type v} :

α ⊕ β → option β

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

Equations

(sum.inr b).get_right = option.some b
(sum.inl _x).get_right = option.none

@[simp]

def sum.is_left {α : Type u} {β : Type v} :

α ⊕ β → bool

Check if a sum is inl.

Equations

(sum.inr _x).is_left = bool.ff
(sum.inl _x).is_left = bool.tt

@[simp]

def sum.is_right {α : Type u} {β : Type v} :

α ⊕ β → bool

Check if a sum is inr.

Equations

(sum.inr _x).is_right = bool.tt
(sum.inl _x).is_right = bool.ff

@[simp]

theorem sum.get_left_eq_none_iff {α : Type u} {β : Type v} {x : α ⊕ β} :

x.get_left = option.none ↔ ↥(x.is_right)

@[simp]

theorem sum.get_right_eq_none_iff {α : Type u} {β : Type v} {x : α ⊕ β} :

x.get_right = option.none ↔ ↥(x.is_left)

@[simp]

theorem sum.get_left_eq_some_iff {α : Type u} {β : Type v} {x : α ⊕ β} {a : α} :

x.get_left = option.some a ↔ x = sum.inl a

@[simp]

theorem sum.get_right_eq_some_iff {α : Type u} {β : Type v} {x : α ⊕ β} {b : β} :

x.get_right = option.some b ↔ x = sum.inr b

@[simp]

theorem sum.bnot_is_left {α : Type u} {β : Type v} (x : α ⊕ β) :

!x.is_left = x.is_right

@[simp]

theorem sum.is_left_eq_ff {α : Type u} {β : Type v} {x : α ⊕ β} :

x.is_left = bool.ff ↔ ↥(x.is_right)

theorem sum.not_is_left {α : Type u} {β : Type v} {x : α ⊕ β} :

¬↥(x.is_left) ↔ ↥(x.is_right)

@[simp]

theorem sum.bnot_is_right {α : Type u} {β : Type v} (x : α ⊕ β) :

!x.is_right = x.is_left

@[simp]

theorem sum.is_right_eq_ff {α : Type u} {β : Type v} {x : α ⊕ β} :

x.is_right = bool.ff ↔ ↥(x.is_left)

theorem sum.not_is_right {α : Type u} {β : Type v} {x : α ⊕ β} :

¬↥(x.is_right) ↔ ↥(x.is_left)

theorem sum.is_left_iff {α : Type u} {β : Type v} {x : α ⊕ β} :

↥(x.is_left) ↔ ∃ (y : α), x = sum.inl y

theorem sum.is_right_iff {α : Type u} {β : Type v} {x : α ⊕ β} :

↥(x.is_right) ↔ ∃ (y : β), x = sum.inr y

theorem sum.inl.inj_iff {α : Type u} {β : Type v} {a b : α} :

sum.inl a = sum.inl b ↔ a = b

theorem sum.inr.inj_iff {α : Type u} {β : Type v} {a b : β} :

sum.inr a = sum.inr b ↔ a = b

theorem sum.inl_ne_inr {α : Type u} {β : Type v} {a : α} {b : β} :

sum.inl a ≠ sum.inr b

theorem sum.inr_ne_inl {α : Type u} {β : Type v} {a : α} {b : β} :

sum.inr b ≠ sum.inl a

@[protected]

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

sum.elim f g = λ (x : α ⊕ β), x.rec_on f g

@[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

@[protected]

def sum.map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : α → α') (g : β → β') :

α ⊕ β → α' ⊕ β'

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

Equations

sum.map f g = sum.elim (sum.inl ∘ f) (sum.inr ∘ g)

@[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.is_left_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ) :

(sum.map f g x).is_left = x.is_left

@[simp]

theorem sum.is_right_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ) :

(sum.map f g x).is_right = x.is_right

@[simp]

theorem sum.get_left_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ) :

(sum.map f g x).get_left = option.map f x.get_left

@[simp]

theorem sum.get_right_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (f : α → β) (g : γ → δ) (x : α ⊕ γ) :

(sum.map f g x).get_right = option.map g x.get_right

@[simp]

theorem sum.update_elim_inl {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq α] [decidable_eq (α ⊕ β)] {f : α → γ} {g : β → γ} {i : α} {x : γ} :

function.update (sum.elim f g) (sum.inl i) x = sum.elim (function.update f i x) g

@[simp]

theorem sum.update_elim_inr {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq β] [decidable_eq (α ⊕ β)] {f : α → γ} {g : β → γ} {i : β} {x : γ} :

function.update (sum.elim f g) (sum.inr i) x = sum.elim f (function.update g i x)

@[simp]

theorem sum.update_inl_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq α] [decidable_eq (α ⊕ β)] {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} [decidable_eq α] [decidable_eq (α ⊕ β)] {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} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {x : γ} :

function.update f (sum.inl i) x ∘ sum.inr = f ∘ sum.inr

@[simp]

theorem sum.update_inl_apply_inr {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :

function.update f (sum.inl i) x (sum.inr j) = f (sum.inr j)

@[simp]

theorem sum.update_inr_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : β} {x : γ} :

function.update f (sum.inr i) x ∘ sum.inl = f ∘ sum.inl

@[simp]

theorem sum.update_inr_apply_inl {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :

function.update f (sum.inr j) x (sum.inl i) = f (sum.inl i)

@[simp]

theorem sum.update_inr_comp_inr {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq β] [decidable_eq (α ⊕ β)] {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} [decidable_eq β] [decidable_eq (α ⊕ β)] {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

sum.swap = sum.elim sum.inr sum.inl

@[simp]

theorem sum.swap_inl {α : Type u} {β : Type v} (x : α) :

(sum.inl x).swap = sum.inr x

@[simp]

theorem sum.swap_inr {α : Type u} {β : Type v} (x : β) :

(sum.inr x).swap = sum.inl x

@[simp]

theorem sum.swap_swap {α : Type u} {β : Type v} (x : α ⊕ β) :

x.swap.swap = x

@[simp]

theorem sum.swap_swap_eq {α : Type u} {β : Type v} :

sum.swap ∘ sum.swap = id

@[simp]

theorem sum.swap_left_inverse {α : Type u} {β : Type v} :

function.left_inverse sum.swap sum.swap

@[simp]

theorem sum.swap_right_inverse {α : Type u} {β : Type v} :

function.right_inverse sum.swap sum.swap

@[simp]

theorem sum.is_left_swap {α : Type u} {β : Type v} (x : α ⊕ β) :

x.swap.is_left = x.is_right

@[simp]

theorem sum.is_right_swap {α : Type u} {β : Type v} (x : α ⊕ β) :

x.swap.is_right = x.is_left

@[simp]

theorem sum.get_left_swap {α : Type u} {β : Type v} (x : α ⊕ β) :

x.swap.get_left = x.get_right

@[simp]

theorem sum.get_right_swap {α : Type u} {β : Type v} (x : α ⊕ β) :

x.swap.get_right = x.get_left

inductive sum.lift_rel {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} (r : α → γ → Prop) (s : β → δ → Prop) :

α ⊕ β → γ ⊕ δ → Prop

inl : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {a : α} {c : γ}, r a c → sum.lift_rel r s (sum.inl a) (sum.inl c)
inr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {b : β} {d : δ}, s b d → sum.lift_rel r s (sum.inr b) (sum.inr d)

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

Instances for sum.lift_rel

@[simp]

theorem sum.lift_rel_inl_inl {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {a : α} {c : γ} :

sum.lift_rel r s (sum.inl a) (sum.inl c) ↔ r a c

@[simp]

theorem sum.not_lift_rel_inl_inr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {a : α} {d : δ} :

¬sum.lift_rel r s (sum.inl a) (sum.inr d)

@[simp]

theorem sum.not_lift_rel_inr_inl {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {b : β} {c : γ} :

¬sum.lift_rel r s (sum.inr b) (sum.inl c)

@[simp]

theorem sum.lift_rel_inr_inr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {b : β} {d : δ} :

sum.lift_rel r s (sum.inr b) (sum.inr d) ↔ s b d

@[protected, instance]

def sum.lift_rel.decidable {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} [Π (a : α) (c : γ), decidable (r a c)] [Π (b : β) (d : δ), decidable (s b d)] (ab : α ⊕ β) (cd : γ ⊕ δ) :

decidable (sum.lift_rel r s ab cd)

Equations

theorem sum.lift_rel.mono {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r₁ r₂ : α → γ → Prop} {s₁ s₂ : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b) (hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b) (h : sum.lift_rel r₁ s₁ x y) :

sum.lift_rel r₂ s₂ x y

theorem sum.lift_rel.mono_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r₁ r₂ : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (hr : ∀ (a : α) (b : γ), r₁ a b → r₂ a b) (h : sum.lift_rel r₁ s x y) :

sum.lift_rel r₂ s x y

theorem sum.lift_rel.mono_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s₁ s₂ : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (hs : ∀ (a : β) (b : δ), s₁ a b → s₂ a b) (h : sum.lift_rel r s₁ x y) :

sum.lift_rel r s₂ x y

@[protected]

theorem sum.lift_rel.swap {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (h : sum.lift_rel r s x y) :

sum.lift_rel s r x.swap y.swap

@[simp]

theorem sum.lift_rel_swap_iff {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} :

sum.lift_rel s r x.swap y.swap ↔ sum.lift_rel r s x y

inductive sum.lex {α : Type u} {β : Type v} (r : α → α → Prop) (s : β → β → Prop) :

α ⊕ β → α ⊕ β → Prop

inl : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α}, r a₁ a₂ → sum.lex r s (sum.inl a₁) (sum.inl a₂)
inr : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} {b₁ b₂ : β}, s b₁ b₂ → sum.lex r s (sum.inr b₁) (sum.inr b₂)
sep : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} (a : α) (b : β), sum.lex r s (sum.inl a) (sum.inr b)

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

Instances for sum.lex

@[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 (sum.inr b) (sum.inl a)

@[protected, instance]

def sum.lex.decidable_rel {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [decidable_rel r] [decidable_rel s] :

decidable_rel (sum.lex r s)

Equations

sum.lex.decidable_rel (sum.inr b) (sum.inr d) = decidable_of_iff' (s b d) sum.lex_inr_inr
sum.lex.decidable_rel (sum.inr b) (sum.inl c) = decidable.is_false sum.lex_inr_inl
sum.lex.decidable_rel (sum.inl a) (sum.inr d) = decidable.is_true _
sum.lex.decidable_rel (sum.inl a) (sum.inl c) = decidable_of_iff' (r a c) sum.lex_inl_inl

@[protected]

theorem sum.lift_rel.lex {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} {a b : α ⊕ β} (h : sum.lift_rel r s a b) :

sum.lex r s a b

theorem sum.lift_rel_subrelation_lex {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} :

subrelation (sum.lift_rel r s) (sum.lex r s)

theorem sum.lex.mono {α : Type u} {β : Type v} {r₁ r₂ : α → α → Prop} {s₁ s₂ : β → β → Prop} {x y : α ⊕ β} (hr : ∀ (a b : α), r₁ a b → r₂ a b) (hs : ∀ (a b : β), s₁ a b → s₂ 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₁ r₂ : α → α → Prop} {s : β → β → Prop} {x y : α ⊕ β} (hr : ∀ (a b : α), r₁ a b → r₂ 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₁ s₂ : β → β → Prop} {x y : α ⊕ β} (hs : ∀ (a b : β), s₁ a b → s₂ 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 : well_founded r) (hb : well_founded s) :

well_founded (sum.lex r 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) :

function.injective (sum.elim f g)

theorem function.injective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : function.injective f) (hg : function.injective g) :

function.injective (sum.map f g)

theorem function.surjective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : function.surjective f) (hg : function.surjective g) :

function.surjective (sum.map f g)

theorem function.bijective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : function.bijective f) (hg : function.bijective g) :

function.bijective (sum.map f g)

@[simp]

theorem sum.map_injective {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} :

function.injective (sum.map f g) ↔ function.injective f ∧ function.injective g

@[simp]

theorem sum.map_surjective {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} :

function.surjective (sum.map f g) ↔ function.surjective f ∧ function.surjective g

@[simp]

theorem sum.map_bijective {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} :

function.bijective (sum.map f g) ↔ function.bijective f ∧ function.bijective g

theorem sum.elim_const_const {α : Type u} {β : Type v} {γ : Type u_1} (c : γ) :

sum.elim (function.const α c) (function.const β c) = function.const (α ⊕ β) c

@[simp]

theorem sum.elim_lam_const_lam_const {α : Type u} {β : Type v} {γ : Type u_1} (c : γ) :

sum.elim (λ (_x : α), c) (λ (_x : β), c) = λ (_x : α ⊕ β), c

theorem sum.elim_update_left {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq α] [decidable_eq β] (f : α → γ) (g : β → γ) (i : α) (c : γ) :

sum.elim (function.update f i c) g = function.update (sum.elim f g) (sum.inl i) c

theorem sum.elim_update_right {α : Type u} {β : Type v} {γ : Type u_1} [decidable_eq α] [decidable_eq β] (f : α → γ) (g : β → γ) (i : β) (c : γ) :

sum.elim f (function.update g i c) = function.update (sum.elim f g) (sum.inr i) c

Ternary sum #

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

@[simp, reducible]

def sum3.in₀ {α : Type u} {β : Type v} {γ : Type u_1} (a : α) :

α ⊕ β ⊕ γ

The map from the first summand into a ternary sum.

Equations

sum3.in₀ a = sum.inl a

@[simp, reducible]

def sum3.in₁ {α : Type u} {β : Type v} {γ : Type u_1} (b : β) :

α ⊕ β ⊕ γ

The map from the second summand into a ternary sum.

Equations

sum3.in₁ b = sum.inr (sum.inl b)

@[simp, reducible]

def sum3.in₂ {α : Type u} {β : Type v} {γ : Type u_1} (c : γ) :

α ⊕ β ⊕ γ

The map from the third summand into a ternary sum.

Equations

sum3.in₂ c = sum.inr (sum.inr c)