Documentation

Mathlib.Data.Sum.Basic

Most of the former contents of this file have been moved to Batteries.

theorem Sum.exists_sum {α : Type u} {β : Type v} {γ : α βSort u_3} (p : ((ab : α β) → γ ab)Prop) :
(∃ (fab : (ab : α β) → γ ab), p fab) ∃ (fa : (val : α) → γ (Sum.inl val)), ∃ (fb : (val : β) → γ (Sum.inr val)), p fun (t : α β) => Sum.rec fa fb t
theorem Sum.inl_injective {α : Type u} {β : Type v} :
theorem Sum.inr_injective {α : Type u} {β : Type v} :
theorem Sum.sum_rec_congr {α : Type u} {β : Type v} (P : α βSort u_3) (f : (i : α) → P ()) (g : (i : β) → P ()) {x : α β} {y : α β} (h : x = y) :
Sum.rec f g x = cast (Sum.rec f g y)
theorem Sum.eq_left_iff_getLeft_eq {α : Type u} {β : Type v} {x : α β} {a : α} :
x = ∃ (h : x.isLeft = true), x.getLeft h = a
theorem Sum.eq_right_iff_getRight_eq {α : Type u} {β : Type v} {x : α β} {b : β} :
x = ∃ (h : x.isRight = true), x.getRight h = b
theorem Sum.getLeft_eq_getLeft? {α : Type u} {β : Type v} {x : α β} (h₁ : x.isLeft = true) (h₂ : x.getLeft?.isSome = true) :
x.getLeft h₁ = x.getLeft?.get h₂
theorem Sum.getRight_eq_getRight? {α : Type u} {β : Type v} {x : α β} (h₁ : x.isRight = true) (h₂ : x.getRight?.isSome = true) :
x.getRight h₁ = x.getRight?.get h₂
@[simp]
theorem Sum.isSome_getLeft?_iff_isLeft {α : Type u} {β : Type v} {x : α β} :
x.getLeft?.isSome = true x.isLeft = true
@[simp]
theorem Sum.isSome_getRight?_iff_isRight {α : Type u} {β : Type v} {x : α β} :
x.getRight?.isSome = true x.isRight = true
@[simp]
theorem Sum.update_elim_inl {α : Type u} {β : Type v} {γ : Type u_1} [] [DecidableEq (α β)] {f : αγ} {g : βγ} {i : α} {x : γ} :
@[simp]
theorem Sum.update_elim_inr {α : Type u} {β : Type v} {γ : Type u_1} [] [DecidableEq (α β)] {f : αγ} {g : βγ} {i : β} {x : γ} :
@[simp]
theorem Sum.update_inl_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [] [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} [] [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} [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} [DecidableEq (α β)] {f : α βγ} {i : α} {j : β} {x : γ} :
Function.update f () x () = f ()
@[simp]
theorem Sum.update_inr_comp_inl {α : Type u} {β : Type v} {γ : Type u_1} [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} [DecidableEq (α β)] {f : α βγ} {i : α} {j : β} {x : γ} :
Function.update f () x () = f ()
@[simp]
theorem Sum.update_inr_comp_inr {α : Type u} {β : Type v} {γ : Type u_1} [] [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} [] [DecidableEq (α β)] {f : α βγ} {i : β} {j : β} {x : γ} :
Function.update f () x () = Function.update (f Sum.inr) i x j
@[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
theorem Sum.liftRel_iff {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (r : αγProp) (s : βδProp) :
∀ (a : α β) (a_1 : γ δ), Sum.LiftRel r s a a_1 (∃ (a_2 : α), ∃ (c : γ), r a_2 c a = Sum.inl a_2 a_1 = ) ∃ (b : β), ∃ (d : δ), s b d a = a_1 =
theorem Sum.LiftRel.isLeft_congr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} (h : Sum.LiftRel r s x y) :
x.isLeft = true y.isLeft = true
theorem Sum.LiftRel.isRight_congr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} (h : Sum.LiftRel r s x y) :
x.isRight = true y.isRight = true
theorem Sum.LiftRel.isLeft_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {c : γ} (h : Sum.LiftRel r s x ()) :
x.isLeft = true
theorem Sum.LiftRel.isLeft_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {y : γ δ} {a : α} (h : Sum.LiftRel r s () y) :
y.isLeft = true
theorem Sum.LiftRel.isRight_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {d : δ} (h : Sum.LiftRel r s x ()) :
x.isRight = true
theorem Sum.LiftRel.isRight_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {y : γ δ} {b : β} (h : Sum.LiftRel r s () y) :
y.isRight = true
theorem Sum.LiftRel.exists_of_isLeft_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} (h₁ : Sum.LiftRel r s x y) (h₂ : x.isLeft = true) :
∃ (a : α), ∃ (c : γ), r a c x = y =
theorem Sum.LiftRel.exists_of_isLeft_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} (h₁ : Sum.LiftRel r s x y) (h₂ : y.isLeft = true) :
∃ (a : α), ∃ (c : γ), r a c x = y =
theorem Sum.LiftRel.exists_of_isRight_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} (h₁ : Sum.LiftRel r s x y) (h₂ : x.isRight = true) :
∃ (b : β), ∃ (d : δ), s b d x = y =
theorem Sum.LiftRel.exists_of_isRight_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : αγProp} {s : βδProp} {x : α β} {y : γ δ} (h₁ : Sum.LiftRel r s x y) (h₂ : y.isRight = true) :
∃ (b : β), ∃ (d : δ), s b d x = y =
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_1} {δ : Type u_2} {f : αγ} {g : βδ} :
@[simp]
theorem Sum.map_surjective {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : αγ} {g : βδ} :
@[simp]
theorem Sum.map_bijective {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : αγ} {g : βδ} :
theorem Sum.elim_update_left {α : Type u} {β : Type v} {γ : Type u_1} [] [] (f : αγ) (g : βγ) (i : α) (c : γ) :
theorem Sum.elim_update_right {α : Type u} {β : Type v} {γ : Type u_1} [] [] (f : αγ) (g : βγ) (i : β) (c : γ) :

Ternary sum #

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

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

The map from the first summand into a ternary sum.

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

The map from the second summand into a ternary sum.

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

The map from the third summand into a ternary sum.

Equations
Instances For