Additional lemmas about sum types #
Most of the former contents of this file have been moved to Std.
theorem
Sum.eq_left_iff_getLeft_eq
{α : Type u}
{β : Type v}
{x : α ⊕ β}
{a : α}
:
x = Sum.inl a ↔ ∃ h, Sum.getLeft x h = a
theorem
Sum.eq_right_iff_getRight_eq
{α : Type u}
{β : Type v}
{x : α ⊕ β}
{b : β}
:
x = Sum.inr b ↔ ∃ h, Sum.getRight x h = b
theorem
Sum.getLeft_eq_getLeft?
{α : Type u}
{β : Type v}
{x : α ⊕ β}
(h₁ : Sum.isLeft x = true)
(h₂ : Option.isSome (Sum.getLeft? x) = true)
:
Sum.getLeft x h₁ = Option.get (Sum.getLeft? x) h₂
theorem
Sum.getRight_eq_getRight?
{α : Type u}
{β : Type v}
{x : α ⊕ β}
(h₁ : Sum.isRight x = true)
(h₂ : Option.isSome (Sum.getRight? x) = true)
:
Sum.getRight x h₁ = Option.get (Sum.getRight? x) h₂
@[simp]
theorem
Sum.isSome_getLeft?_iff_isLeft
{α : Type u}
{β : Type v}
{x : α ⊕ β}
:
Option.isSome (Sum.getLeft? x) = true ↔ Sum.isLeft x = true
@[simp]
theorem
Sum.isSome_getRight?_iff_isRight
{α : Type u}
{β : Type v}
{x : α ⊕ β}
:
Option.isSome (Sum.getRight? x) = true ↔ Sum.isRight x = true
@[simp]
theorem
Sum.update_elim_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq α]
[DecidableEq (α ⊕ β)]
{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}
[DecidableEq β]
[DecidableEq (α ⊕ β)]
{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}
[DecidableEq α]
[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}
[DecidableEq α]
[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}
[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}
[DecidableEq (α ⊕ β)]
{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}
[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}
[DecidableEq (α ⊕ β)]
{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}
[DecidableEq β]
[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}
[DecidableEq β]
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : β}
{j : β}
{x : γ}
:
Function.update f (Sum.inr i) x (Sum.inr j) = Function.update (f ∘ Sum.inr) i x j
@[simp]
@[simp]
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 : β → δ}
:
@[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}
[DecidableEq α]
[DecidableEq β]
(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}
[DecidableEq α]
[DecidableEq β]
(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.