Additional lemmas about sum types #
Most of the former contents of this file have been moved to Batteries.
theorem
not_isLeft_and_isRight
{α : Type u}
{β : Type v}
{x : α ⊕ β}
:
¬(x.isLeft = true ∧ x.isRight = true)
@[simp]
theorem
Sum.elim_swap
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → γ}
{g : β → γ}
:
Sum.elim f g ∘ swap = Sum.elim g f
theorem
Sum.sum_rec_congr
{α : Type u}
{β : Type v}
(P : α ⊕ β → Sort u_3)
(f : (i : α) → P (inl i))
(g : (i : β) → P (inr i))
{x y : α ⊕ β}
(h : x = y)
:
rec f g x = cast ⋯ (rec f g y)
theorem
Sum.eq_left_iff_getLeft_eq
{α : Type u}
{β : Type v}
{x : α ⊕ β}
{a : α}
:
x = inl a ↔ ∃ (h : x.isLeft = true), x.getLeft h = a
theorem
Sum.eq_right_iff_getRight_eq
{α : Type u}
{β : Type v}
{x : α ⊕ β}
{b : β}
:
x = inr b ↔ ∃ (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 α]
[DecidableEq (α ⊕ β)]
{f : α → γ}
{g : β → γ}
{i : α}
{x : γ}
:
Function.update (Sum.elim f g) (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) (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 (inl i) x ∘ inl = Function.update (f ∘ 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 (inl i) x (inl j) = Function.update (f ∘ 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 (inl i) x ∘ inr = f ∘ inr
theorem
Sum.update_inl_apply_inr
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : α}
{j : β}
{x : γ}
:
Function.update f (inl i) x (inr j) = f (inr j)
@[simp]
theorem
Sum.update_inr_comp_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : β}
{x : γ}
:
Function.update f (inr i) x ∘ inl = f ∘ inl
theorem
Sum.update_inr_apply_inl
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : α}
{j : β}
{x : γ}
:
Function.update f (inr j) x (inl i) = f (inl i)
@[simp]
theorem
Sum.update_inr_comp_inr
{α : Type u}
{β : Type v}
{γ : Type u_1}
[DecidableEq β]
[DecidableEq (α ⊕ β)]
{f : α ⊕ β → γ}
{i : β}
{x : γ}
:
Function.update f (inr i) x ∘ inr = Function.update (f ∘ 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 (inr i) x (inr j) = Function.update (f ∘ inr) i x j
@[simp]
theorem
Sum.update_inl_apply_inl'
{α : Type u}
{β : Type v}
{γ : α ⊕ β → Type u_3}
[DecidableEq α]
[DecidableEq (α ⊕ β)]
{f : (i : α ⊕ β) → γ i}
{i : α}
{x : γ (inl i)}
(j : α)
:
Function.update f (inl i) x (inl j) = Function.update (fun (j : α) => f (inl j)) i x 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 : β)
:
Function.update f (inr i) x (inr j) = Function.update (fun (j : β) => f (inr j)) i x 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 : γ)
:
Sum.elim (Function.update f a x) g = Function.update (Sum.elim f g) (inl a) x
@[simp]
theorem
Sum.elim_update_right
{α : Type u}
{β : Type v}
{γ : Sort u_3}
[DecidableEq α]
[DecidableEq β]
(f : α → γ)
(g : β → γ)
(b : β)
(x : γ)
:
Sum.elim f (Function.update g b x) = Function.update (Sum.elim f g) (inr b) x
@[simp]
@[simp]
theorem
Function.Injective.sumElim
{α : Type u}
{β : Type v}
{γ : Sort u_3}
{f : α → γ}
{g : β → γ}
(hf : Injective f)
(hg : Injective g)
(hfg : ∀ (a : α) (b : β), f a ≠ g b)
:
Injective (Sum.elim f g)
@[simp]
theorem
Sum.elim_injective
{α : Type u}
{β : Type v}
{γ : Sort u_3}
{f : α → γ}
{g : β → γ}
:
Function.Injective (Sum.elim f g) ↔ Function.Injective f ∧ Function.Injective g ∧ ∀ (a : α) (b : β), f a ≠ g b
@[simp]
theorem
Sum.elim_injective'
{α : Type u}
{β : Type v}
{γ : Sort u_3}
{f : α → γ}
:
Function.Injective (Sum.elim f)
@[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
Ternary sum #
Abbreviations for the maps from the summands to α ⊕ β ⊕ γ. This is useful for pattern-matching.