Additional lemmas about sum types #
Most of the former contents of this file have been moved to Batteries.
@[simp]
theorem
Sum.update_elim_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq α]
[DecidableEq (α ⊕ β)]
{f : α → γ}
{g : β → γ}
{i : α}
{x : γ}
:
@[simp]
theorem
Sum.update_elim_inr
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq β]
[DecidableEq (α ⊕ β)]
{f : α → γ}
{g : β → γ}
{i : β}
{x : γ}
:
@[simp]
theorem
Sum.update_inl_comp_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq α]
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : α}
{x : γ}
:
@[simp]
theorem
Sum.update_inl_apply_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq α]
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i j : α}
{x : γ}
:
@[simp]
theorem
Sum.update_inl_comp_inr
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : α}
{x : γ}
:
theorem
Sum.update_inl_apply_inr
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : α}
{j : β}
{x : γ}
:
@[simp]
theorem
Sum.update_inr_comp_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : β}
{x : γ}
:
theorem
Sum.update_inr_apply_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : α}
{j : β}
{x : γ}
:
@[simp]
theorem
Sum.update_inr_comp_inr
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq β]
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : β}
{x : γ}
:
@[simp]
theorem
Sum.update_inr_apply_inr
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq β]
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i j : β}
{x : γ}
:
@[simp]
theorem
Sum.update_inl_apply_inl'
{α : Type u}
{β : Type v}
{γ : α ⊕ β → Type u_3}
[DecidableEq α]
[DecidableEq (α ⊕ β)]
{f : (i : α ⊕ β) → γ i}
{i : α}
{x : γ (inl i)}
(j : α)
:
@[simp]
theorem
Sum.update_inr_apply_inr'
{α : Type u}
{β : Type v}
{γ : α ⊕ β → Type u_3}
[DecidableEq β]
[DecidableEq (α ⊕ β)]
{f : (i : α ⊕ β) → γ i}
{i : β}
{x : γ (inr i)}
(j : β)
:
@[simp]
theorem
Sum.rec_update_left
{α : Type u}
{β : Type v}
{γ : α ⊕ β → Sort u_3}
[DecidableEq α]
[DecidableEq β]
(f : (a : α) → γ (inl a))
(g : (b : β) → γ (inr b))
(a : α)
(x : γ (inl a))
:
(fun (t : α ⊕ β) => rec (Function.update f a x) g t) = Function.update (fun (t : α ⊕ β) => rec f g t) (inl a) x
@[simp]
theorem
Sum.rec_update_right
{α : Type u}
{β : Type v}
{γ : α ⊕ β → Sort u_3}
[DecidableEq α]
[DecidableEq β]
(f : (a : α) → γ (inl a))
(g : (b : β) → γ (inr b))
(b : β)
(x : γ (inr b))
:
(fun (t : α ⊕ β) => rec f (Function.update g b x) t) = Function.update (fun (t : α ⊕ β) => rec f g t) (inr b) x
@[simp]
theorem
Sum.elim_update_left
{α : Type u}
{β : Type v}
{γ : Sort u_3}
[DecidableEq α]
[DecidableEq β]
(f : α → γ)
(g : β → γ)
(a : α)
(x : γ)
:
@[simp]
theorem
Sum.elim_update_right
{α : Type u}
{β : Type v}
{γ : Sort u_3}
[DecidableEq α]
[DecidableEq β]
(f : α → γ)
(g : β → γ)
(b : β)
(x : γ)
:
@[simp]
@[simp]
@[deprecated Function.Injective.sumElim (since := "2025-02-20")]
theorem
Function.Injective.sum_elim
{α : Type u}
{β : Type v}
{γ : Type u_1}
{f : α → γ}
{g : β → γ}
(hf : Injective f)
(hg : Injective g)
(hfg : ∀ (a : α) (b : β), f a ≠ g b)
:
Alias of Function.Injective.sumElim
.
theorem
Function.Surjective.sumMap
{α : Type u}
{α' : Type w}
{β : Type v}
{β' : Type x}
{f : α → β}
{g : α' → β'}
(hf : Surjective f)
(hg : Surjective g)
:
Surjective (Sum.map f g)
@[deprecated Function.Surjective.sumMap (since := "2025-02-20")]
theorem
Function.Surjective.sum_map
{α : Type u}
{α' : Type w}
{β : Type v}
{β' : Type x}
{f : α → β}
{g : α' → β'}
(hf : Surjective f)
(hg : Surjective g)
:
Surjective (Sum.map f g)
Alias of Function.Surjective.sumMap
.
@[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 : β → δ}
:
Ternary sum #
Abbreviations for the maps from the summands to α ⊕ β ⊕ γ
. This is useful for pattern-matching.