Disjoint union of types

Theorems about the definitions introduced in Init.Data.Sum.Basic.

theorem Sum.forall {α : Type u_1} {β : Type u_2} {p : α ⊕ β → Prop} : (∀ (x : α ⊕ β), p x) ↔ (∀ (a : α), p (inl a)) ∧ ∀ (b : β), p (inr b)

theorem Sum.exists {α : Type u_1} {β : Type u_2} {p : α ⊕ β → Prop} : (∃ (x : α ⊕ β), p x) ↔ (∃ (a : α), p (inl a)) ∨ ∃ (b : β), p (inr b)

theorem Sum.forall_sum {α : Type u_1} {β : Type u_2} {γ : α ⊕ β → 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

@[simp]

theorem Sum.inl_getLeft {α : Type u_1} {β : Type u_2} (x : α ⊕ β) (h : x.isLeft = true) : inl (x.getLeft h) = x

@[simp]

theorem Sum.inr_getRight {α : Type u_1} {β : Type u_2} (x : α ⊕ β) (h : x.isRight = true) : inr (x.getRight h) = x

@[simp]

theorem Sum.getLeft?_eq_none_iff {α : Type u_1} {β : Type u_2} {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight = true

@[simp]

theorem Sum.getRight?_eq_none_iff {α : Type u_1} {β : Type u_2} {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft = true

theorem Sum.eq_left_getLeft_of_isLeft {α : Type u_1} {β : Type u_2} {x : α ⊕ β} (h : x.isLeft = true) : x = inl (x.getLeft h)

@[simp]

theorem Sum.getLeft_eq_iff {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {x : α✝ ⊕ β✝} (h : x.isLeft = true) : x.getLeft h = a ↔ x = inl a

theorem Sum.eq_right_getRight_of_isRight {α : Type u_1} {β : Type u_2} {x : α ⊕ β} (h : x.isRight = true) : x = inr (x.getRight h)

@[simp]

theorem Sum.getRight_eq_iff {β✝ : Type u_1} {b : β✝} {α✝ : Type u_2} {x : α✝ ⊕ β✝} (h : x.isRight = true) : x.getRight h = b ↔ x = inr b

@[simp]

theorem Sum.getLeft?_eq_some_iff {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {x : α✝ ⊕ β✝} : x.getLeft? = some a ↔ x = inl a

@[simp]

theorem Sum.getRight?_eq_some_iff {β✝ : Type u_1} {b : β✝} {α✝ : Type u_2} {x : α✝ ⊕ β✝} : x.getRight? = some b ↔ x = inr b

@[simp]

theorem Sum.bnot_isLeft {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : (!decide (x.isLeft = x.isRight)) = true

@[simp]

theorem Sum.isLeft_eq_false {α : Type u_1} {β : Type u_2} {x : α ⊕ β} : x.isLeft = false ↔ x.isRight = true

theorem Sum.not_isLeft {α : Type u_1} {β : Type u_2} {x : α ⊕ β} : ¬x.isLeft = true ↔ x.isRight = true

@[simp]

theorem Sum.bnot_isRight {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : (!decide (x.isRight = x.isLeft)) = true

@[simp]

theorem Sum.isRight_eq_false {α : Type u_1} {β : Type u_2} {x : α ⊕ β} : x.isRight = false ↔ x.isLeft = true

theorem Sum.not_isRight {α : Type u_1} {β : Type u_2} {x : α ⊕ β} : ¬x.isRight = true ↔ x.isLeft = true

theorem Sum.isLeft_iff {α✝ : Type u_1} {β✝ : Type u_2} {x : α✝ ⊕ β✝} : x.isLeft = true ↔ ∃ (y : α✝), x = inl y

theorem Sum.isRight_iff {α✝ : Type u_1} {β✝ : Type u_2} {x : α✝ ⊕ β✝} : x.isRight = true ↔ ∃ (y : β✝), x = inr y

theorem Sum.inl.inj_iff {α : Type u_1} {β : Type u_2} {a b : α} : inl a = inl b ↔ a = b

theorem Sum.inr.inj_iff {α : Type u_1} {β : Type u_2} {a b : β} : inr a = inr b ↔ a = b

theorem Sum.inl_ne_inr {α✝ : Type u_1} {a : α✝} {β✝ : Type u_2} {b : β✝} : inl a ≠ inr b

theorem Sum.inr_ne_inl {β✝ : Type u_1} {b : β✝} {α✝ : Type u_2} {a : α✝} : inr b ≠ inl a

Sum.elim

@[simp]

theorem Sum.elim_comp_inl {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inl = f

@[simp]

theorem Sum.elim_comp_inr {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inr = g

@[simp]

theorem Sum.elim_inl_inr {α : Type u_1} {β : Type u_2} : Sum.elim inl inr = id

theorem Sum.comp_elim {γ : Sort u_1} {δ : Sort u_2} {α : Type u_3} {β : Type u_4} (f : γ → δ) (g : α → γ) (h : β → γ) : f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h)

@[simp]

theorem Sum.elim_comp_inl_inr {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α ⊕ β → γ) : Sum.elim (f ∘ inl) (f ∘ inr) = f

theorem Sum.elim_eq_iff {α : Type u_1} {γ : Sort u_2} {β : Type u_3} {u u' : α → γ} {v v' : β → γ} : Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v'

Sum.map

@[simp]

theorem Sum.map_map {α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') (x : α ⊕ β) : Sum.map f' g' (Sum.map f g x) = Sum.map (f' ∘ f) (g' ∘ g) x

@[simp]

theorem Sum.map_comp_map {α' : Type u_1} {α'' : Type u_2} {β' : Type u_3} {β'' : Type u_4} {α : Type u_5} {β : Type u_6} (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') : Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g)

@[simp]

theorem Sum.map_id_id {α : Type u_1} {β : Type u_2} : Sum.map id id = id

theorem Sum.elim_map {α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x : α ⊕ γ} : Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x

theorem Sum.elim_comp_map {α : Type u_1} {β : Type u_2} {ε : Sort u_3} {γ : Type u_4} {δ : Type u_5} {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} : Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁)

@[simp]

theorem Sum.isLeft_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).isLeft = x.isLeft

@[simp]

theorem Sum.isRight_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).isRight = x.isRight

@[simp]

theorem Sum.getLeft?_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).getLeft? = Option.map f x.getLeft?

@[simp]

theorem Sum.getRight?_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ) : (Sum.map f g x).getRight? = Option.map g x.getRight?

Sum.swap

@[simp]

theorem Sum.swap_swap {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : x.swap.swap = x

@[simp]

theorem Sum.swap_swap_eq {α : Type u_1} {β : Type u_2} : swap ∘ swap = id

@[simp]

theorem Sum.isLeft_swap {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : x.swap.isLeft = x.isRight

@[simp]

theorem Sum.isRight_swap {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : x.swap.isRight = x.isLeft

@[simp]

theorem Sum.getLeft?_swap {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : x.swap.getLeft? = x.getRight?

@[simp]

theorem Sum.getRight?_swap {α : Type u_1} {β : Type u_2} (x : α ⊕ β) : x.swap.getRight? = x.getLeft?

theorem Sum.LiftRel.mono {α✝ : Type u_1} {α✝¹ : Type u_2} {r₁ r₂ : α✝ → α✝¹ → Prop} {β✝ : Type u_3} {β✝¹ : Type u_4} {s₁ s₂ : β✝ → β✝¹ → Prop} {x : α✝ ⊕ β✝} {y : α✝¹ ⊕ β✝¹} (hr : ∀ (a : α✝) (b : α✝¹), r₁ a b → r₂ a b) (hs : ∀ (a : β✝) (b : β✝¹), s₁ a b → s₂ a b) (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y

theorem Sum.LiftRel.mono_left {α✝ : Type u_1} {α✝¹ : Type u_2} {r₁ r₂ : α✝ → α✝¹ → Prop} {β✝ : Type u_3} {β✝¹ : Type u_4} {s : β✝ → β✝¹ → Prop} {x : α✝ ⊕ β✝} {y : α✝¹ ⊕ β✝¹} (hr : ∀ (a : α✝) (b : α✝¹), r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) : LiftRel r₂ s x y

theorem Sum.LiftRel.mono_right {β✝ : Type u_1} {β✝¹ : Type u_2} {s₁ s₂ : β✝ → β✝¹ → Prop} {α✝ : Type u_3} {α✝¹ : Type u_4} {r : α✝ → α✝¹ → Prop} {x : α✝ ⊕ β✝} {y : α✝¹ ⊕ β✝¹} (hs : ∀ (a : β✝) (b : β✝¹), s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) : LiftRel r s₂ x y

theorem Sum.LiftRel.swap {α✝ : Type u_1} {α✝¹ : Type u_2} {r : α✝ → α✝¹ → Prop} {β✝ : Type u_3} {β✝¹ : Type u_4} {s : β✝ → β✝¹ → Prop} {x : α✝ ⊕ β✝} {y : α✝¹ ⊕ β✝¹} (h : LiftRel r s x y) : LiftRel s r x.swap y.swap

@[simp]

theorem Sum.liftRel_swap_iff {β✝ : Type u_1} {β✝¹ : Type u_2} {s : β✝ → β✝¹ → Prop} {α✝ : Type u_3} {α✝¹ : Type u_4} {r : α✝ → α✝¹ → Prop} {x : α✝ ⊕ β✝} {y : α✝¹ ⊕ β✝¹} : LiftRel s r x.swap y.swap ↔ LiftRel r s x y

theorem Sum.LiftRel.lex {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b

theorem Sum.liftRel_subrelation_lex {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {β✝ : Type u_2} {s : β✝ → β✝ → Prop} : Subrelation (LiftRel r s) (Lex r s)

theorem Sum.Lex.mono {α✝ : Type u_1} {r₁ r₂ : α✝ → α✝ → Prop} {β✝ : Type u_2} {s₁ s₂ : β✝ → β✝ → Prop} {x y : α✝ ⊕ β✝} (hr : ∀ (a b : α✝), r₁ a b → r₂ a b) (hs : ∀ (a b : β✝), s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) : Lex r₂ s₂ x y

theorem Sum.Lex.mono_left {α✝ : Type u_1} {r₁ r₂ : α✝ → α✝ → Prop} {β✝ : Type u_2} {s : β✝ → β✝ → Prop} {x y : α✝ ⊕ β✝} (hr : ∀ (a b : α✝), r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y

theorem Sum.Lex.mono_right {β✝ : Type u_1} {s₁ s₂ : β✝ → β✝ → Prop} {α✝ : Type u_2} {r : α✝ → α✝ → Prop} {x y : α✝ ⊕ β✝} (hs : ∀ (a b : β✝), s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y

theorem Sum.lex_acc_inl {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {a : α✝} {β✝ : Type u_2} {s : β✝ → β✝ → Prop} (aca : Acc r a) : Acc (Lex r s) (inl a)

theorem Sum.lex_acc_inr {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {β✝ : Type u_2} {s : β✝ → β✝ → Prop} (aca : ∀ (a : α✝), Acc (Lex r s) (inl a)) {b : β✝} (acb : Acc s b) : Acc (Lex r s) (inr b)

theorem Sum.lex_wf {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {α✝¹ : Type u_2} {s : α✝¹ → α✝¹ → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s)

theorem Sum.elim_const_const {γ : Sort u_1} {α : Type u_2} {β : Type u_3} (c : γ) : Sum.elim (Function.const α c) (Function.const β c) = Function.const (α ⊕ β) c

@[simp]

theorem Sum.elim_lam_const_lam_const {γ : Sort u_1} {α : Type u_2} {β : Type u_3} (c : γ) : (Sum.elim (fun (x : α) => c) fun (x : β) => c) = fun (x : α ⊕ β) => c