Additional lemmas about sum types #

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 : α) → γ (inl val)), ∃ (fb : (val : β) → γ (inr val)), p fun (t : α ⊕ β) => rec fa fb t

source

theorem Sum.inl_injective {α : Type u} {β : Type v} :

Function.Injective inl

source

theorem Sum.inr_injective {α : Type u} {β : Type v} :

Function.Injective inr

source

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)

source

theorem Sum.eq_left_iff_getLeft_eq {α : Type u} {β : Type v} {x : α ⊕ β} {a : α} :

x = inl a ↔ ∃ (h : x.isLeft = true), x.getLeft h = a

source

theorem Sum.eq_right_iff_getRight_eq {α : Type u} {β : Type v} {x : α ⊕ β} {b : β} :

x = inr b ↔ ∃ (h : x.isRight = true), x.getRight h = b

source

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₂

source

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₂

source

@[simp]

theorem Sum.isSome_getLeft?_iff_isLeft {α : Type u} {β : Type v} {x : α ⊕ β} :

x.getLeft?.isSome = true ↔ x.isLeft = true

source

@[simp]

theorem Sum.isSome_getRight?_iff_isRight {α : Type u} {β : Type v} {x : α ⊕ β} :

x.getRight?.isSome = true ↔ x.isRight = true

source

@[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

source

@[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)

source

@[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

source

@[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

source

@[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

source

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)

source

@[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

source

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)

source

@[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

source

@[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

source

@[simp]

theorem Sum.swap_leftInverse {α : Type u} {β : Type v} :

Function.LeftInverse swap swap

source

@[simp]

theorem Sum.swap_rightInverse {α : Type u} {β : Type v} :

Function.RightInverse swap swap

source

theorem Sum.liftRel_iff {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (r : α → γ → Prop) (s : β → δ → Prop) (a✝ : α ⊕ β) (a✝¹ : γ ⊕ δ) :

LiftRel r s a✝ a✝¹ ↔ (∃ (a : α), ∃ (c : γ), r a c ∧ a✝ = inl a ∧ a✝¹ = inl c) ∨ ∃ (b : β), ∃ (d : δ), s b d ∧ a✝ = inr b ∧ a✝¹ = inr d

source

theorem Sum.LiftRel.isLeft_congr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (h : LiftRel r s x y) :

x.isLeft = true ↔ y.isLeft = true

source

theorem Sum.LiftRel.isRight_congr {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (h : LiftRel r s x y) :

x.isRight = true ↔ y.isRight = true

source

theorem Sum.LiftRel.isLeft_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {c : γ} (h : LiftRel r s x (inl c)) :

x.isLeft = true

source

theorem Sum.LiftRel.isLeft_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {y : γ ⊕ δ} {a : α} (h : LiftRel r s (inl a) y) :

y.isLeft = true

source

theorem Sum.LiftRel.isRight_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {d : δ} (h : LiftRel r s x (inr d)) :

x.isRight = true

source

theorem Sum.LiftRel.isRight_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {y : γ ⊕ δ} {b : β} (h : LiftRel r s (inr b) y) :

y.isRight = true

source

theorem Sum.LiftRel.exists_of_isLeft_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (h₁ : LiftRel r s x y) (h₂ : x.isLeft = true) :

∃ (a : α), ∃ (c : γ), r a c ∧ x = inl a ∧ y = inl c

source

theorem Sum.LiftRel.exists_of_isLeft_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (h₁ : LiftRel r s x y) (h₂ : y.isLeft = true) :

∃ (a : α), ∃ (c : γ), r a c ∧ x = inl a ∧ y = inl c

source

theorem Sum.LiftRel.exists_of_isRight_left {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (h₁ : LiftRel r s x y) (h₂ : x.isRight = true) :

∃ (b : β), ∃ (d : δ), s b d ∧ x = inr b ∧ y = inr d

source

theorem Sum.LiftRel.exists_of_isRight_right {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {r : α → γ → Prop} {s : β → δ → Prop} {x : α ⊕ β} {y : γ ⊕ δ} (h₁ : LiftRel r s x y) (h₂ : y.isRight = true) :

∃ (b : β), ∃ (d : δ), s b d ∧ x = inr b ∧ y = inr d

source

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) :

Injective (Sum.elim f g)

source

theorem Function.Injective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Injective f) (hg : Injective g) :

Injective (Sum.map f g)

source

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)

source

theorem Function.Bijective.sum_map {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'} (hf : Bijective f) (hg : Bijective g) :

Bijective (Sum.map f g)

source

@[simp]