Additional lemmas about sum types #

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

source

theorem Sum.exists_sum {α : Type u} {β : Type v} {γ : α ⊕ β → Sort u_3} (p : ((ab : α ⊕ β) → γ ab) → Prop) :

(∃ fab, p fab) ↔ ∃ fa fb, p fun t => Sum.rec fa fb t

source

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

Function.Injective Sum.inl

source

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

Function.Injective Sum.inr

source

theorem Sum.sum_rec_congr {α : Type u} {β : Type v} (P : α ⊕ β → Sort u_3) (f : (i : α) → P (Sum.inl i)) (g : (i : β) → P (Sum.inr i)) {x : α ⊕ β} {y : α ⊕ β} (h : x = y) :

Sum.rec f g x = cast (_ : P y = P x) (Sum.rec f g y)

source

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

x = Sum.inl a ↔ ∃ h, Sum.getLeft x h = a

source

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

x = Sum.inr b ↔ ∃ h, Sum.getRight x h = b

source

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₂

source

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₂

source

@[simp]

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

Option.isSome (Sum.getLeft? x) = true ↔ Sum.isLeft x = true

source

@[simp]

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

Option.isSome (Sum.getRight? x) = true ↔ Sum.isRight x = 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) (Sum.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) (Sum.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 (Sum.inl i) x ∘ Sum.inl = Function.update (f ∘ Sum.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 (Sum.inl i) x (Sum.inl j) = Function.update (f ∘ Sum.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 (Sum.inl i) x ∘ Sum.inr = f ∘ Sum.inr

source

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)

source

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

source

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)

source

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

source

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

source

@[simp]

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

Function.LeftInverse Sum.swap Sum.swap

source

@[simp]

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

Function.RightInverse Sum.swap Sum.swap

source

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)

source

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)

source

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)

source

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)

source

@[simp]

theorem Sum.map_injective {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} :

Function.Injective (Sum.map f g) ↔ Function.Injective f ∧ Function.Injective g

source

@[simp]

theorem Sum.map_surjective {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α → γ} {g : β → δ} :

Function.Surjective (Sum.map f g) ↔ Function.Surjective f ∧ Function.Surjective g

source

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

source

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

source

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.

source

@[match_pattern, reducible]

def Sum3.in₀ {α : Type u} {β : Type v} {γ : Type u_1} (a : α) :

α ⊕ β ⊕ γ

The map from the first summand into a ternary sum.

Equations

Sum3.in₀ a = Sum.inl a

Instances For

source

@[match_pattern, reducible]

def Sum3.in₁ {α : Type u} {β : Type v} {γ : Type u_1} (b : β) :

α ⊕ β ⊕ γ

The map from the second summand into a ternary sum.

Equations

Sum3.in₁ b = Sum.inr (Sum.inl b)

Instances For

source

@[match_pattern, reducible]

def Sum3.in₂ {α : Type u} {β : Type v} {γ : Type u_1} (c : γ) :

α ⊕ β ⊕ γ

The map from the third summand into a ternary sum.

Equations

Sum3.in₂ c = Sum.inr (Sum.inr c)

Instances For