mathlib documentation

data.sum

More theorems about the sum type #

source
@[simp]
def sum.get_left {α : Type u_1} {β : Type u_2} :
α ⊕ β → option α

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

Equations
source
@[simp]
def sum.get_right {α : Type u_1} {β : Type u_2} :
α ⊕ β → option β

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

Equations
source
@[simp]
def sum.is_left {α : Type u_1} {β : Type u_2} :
α ⊕ β → bool

Check if a sum is inl.

Equations
source
@[simp]
def sum.is_right {α : Type u_1} {β : Type u_2} :
α ⊕ β → bool

Check if a sum is inr.

Equations
source
@[protected, instance]
def sum.decidable_eq (α : Type u) [a : decidable_eq α] (β : Type v) [a_1 : decidable_eq β] :
decidable_eq (α ⊕ β)
source
@[simp]
theorem sum.forall {α : Type u} {β : Type v} {p : α ⊕ β → Prop} :
(∀ (x : α ⊕ β), p x) ↔ (∀ (a : α), p (sum.inl a)) ∧ ∀ (b : β), p (sum.inr b)
source
@[simp]
theorem sum.exists {α : Type u} {β : Type v} {p : α ⊕ β → Prop} :
(∃ (x : α ⊕ β), p x) ↔ (∃ (a : α), p (sum.inl a)) ∨ ∃ (b : β), p (sum.inr b)
source
theorem sum.inl_injective {α : Type u} {β : Type v} :
function.injective sum.inl
source
theorem sum.inr_injective {α : Type u} {β : Type v} :
function.injective sum.inr
source
@[protected]
def sum.map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} (f : α → α') (g : β → β') :
α ⊕ β → α' ⊕ β'

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

Equations
source
@[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)
source
@[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)
source
@[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
source
@[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)
source
@[simp]
theorem sum.map_id_id (α : Type u_1) (β : Type u_2) :
sum.map id id = id
source
theorem sum.inl.inj_iff {α : Type u} {β : Type v} {a b : α} :
sum.inl a = sum.inl b ↔ a = b
source
theorem sum.inr.inj_iff {α : Type u} {β : Type v} {a b : β} :
sum.inr a = sum.inr b ↔ a = b
source
theorem sum.inl_ne_inr {α : Type u} {β : Type v} {a : α} {b : β} :
sum.inl a ≠ sum.inr b
source
theorem sum.inr_ne_inl {α : Type u} {β : Type v} {a : α} {b : β} :
sum.inr b ≠ sum.inl a
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem sum.elim_comp_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) :
sum.elim f g ∘ sum.inl = f
source
@[simp]
theorem sum.elim_comp_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) :
sum.elim f g ∘ sum.inr = g
source
@[simp]
theorem sum.elim_inl_inr {α : Type u_1} {β : Type u_2} :
sum.elim sum.inl sum.inr = id
source
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)
source
@[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
source
@[simp]
theorem sum.update_elim_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [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
source
@[simp]
theorem sum.update_elim_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [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)
source
@[simp]
theorem sum.update_inl_comp_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [decidable_eq α] [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {x : γ} :
function.update f (sum.inl i) x ∘ sum.inl = function.update (f ∘ sum.inl) i x
source
@[simp]
theorem sum.update_inl_apply_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [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
source
@[simp]
theorem sum.update_inl_comp_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {x : γ} :
function.update f (sum.inl i) x ∘ sum.inr = f ∘ sum.inr
source
@[simp]
theorem sum.update_inl_apply_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :
function.update f (sum.inl i) x (sum.inr j) = f (sum.inr j)
source
@[simp]
theorem sum.update_inr_comp_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : β} {x : γ} :
function.update f (sum.inr i) x ∘ sum.inl = f ∘ sum.inl
source
@[simp]
theorem sum.update_inr_apply_inl {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {j : β} {x : γ} :
function.update f (sum.inr j) x (sum.inl i) = f (sum.inl i)
source
@[simp]
theorem sum.update_inr_comp_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [decidable_eq β] [decidable_eq (α ⊕ β)] {f : α ⊕ β → γ} {i : β} {x : γ} :
function.update f (sum.inr i) x ∘ sum.inr = function.update (f ∘ sum.inr) i x
source
@[simp]
theorem sum.update_inr_apply_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} [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
source
inductive sum.lex {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) :
α ⊕ β → α ⊕ β → Prop
  • inl : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) {a₁ a₂ : α}, ra a₁ a₂ → sum.lex ra rb (sum.inl a₁) (sum.inl a₂)
  • inr : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) {b₁ b₂ : β}, rb b₁ b₂ → sum.lex ra rb (sum.inr b₁) (sum.inr b₂)
  • sep : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) (a : α) (b : β), sum.lex ra rb (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 β.

source
@[simp]
theorem sum.lex_inl_inl {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ a₂ : α} :
sum.lex ra rb (sum.inl a₁) (sum.inl a₂) ↔ ra a₁ a₂
source
@[simp]
theorem sum.lex_inr_inr {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {b₁ b₂ : β} :
sum.lex ra rb (sum.inr b₁) (sum.inr b₂) ↔ rb b₁ b₂
source
@[simp]
theorem sum.lex_inr_inl {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {b : β} {a : α} :
¬sum.lex ra rb (sum.inr b) (sum.inl a)
source
theorem sum.lex_acc_inl {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a : α} (aca : acc ra a) :
acc (sum.lex ra rb) (sum.inl a)
source
theorem sum.lex_acc_inr {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (aca : ∀ (a : α), acc (sum.lex ra rb) (sum.inl a)) {b : β} (acb : acc rb b) :
acc (sum.lex ra rb) (sum.inr b)
source
theorem sum.lex_wf {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (ha : well_founded ra) (hb : well_founded rb) :
well_founded (sum.lex ra rb)
source
@[simp]
def sum.swap {α : Type u} {β : Type v} :
α ⊕ β → β ⊕ α

Swap the factors of a sum type

Equations
source
@[simp]
theorem sum.swap_swap {α : Type u} {β : Type v} (x : α ⊕ β) :
x.swap.swap = x
source
@[simp]
theorem sum.swap_swap_eq {α : Type u} {β : Type v} :
sum.swap ∘ sum.swap = id
source
@[simp]
theorem sum.swap_left_inverse {α : Type u} {β : Type v} :
function.left_inverse sum.swap sum.swap
source
@[simp]
theorem sum.swap_right_inverse {α : Type u} {β : Type v} :
function.right_inverse sum.swap sum.swap
source
theorem function.injective.sum_elim {α : Type u} {β : Type v} {γ : Sort 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)
source
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)
source
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)