Disjoint union of types #

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

source

@[simp]

theorem Sum.forall {α : Type u_1} {β : Type u_2} {p : α ⊕ β → Prop} :

(∀ (x : α ⊕ β), p x) ↔ (∀ (a : α), p (Sum.inl a)) ∧ ∀ (b : β), p (Sum.inr b)

source

@[simp]

theorem Sum.exists {α : Type u_1} {β : Type u_2} {p : α ⊕ β → Prop} :

(∃ (x : α ⊕ β), p x) ↔ (∃ (a : α), p (Sum.inl a)) ∨ ∃ (b : β), p (Sum.inr b)

source

theorem Sum.forall_sum {α : Type u_1} {β : Type u_2} {γ : α ⊕ β → Sort u_3} (p : ((ab : α ⊕ β) → γ ab) → Prop) :

(∀ (fab : (ab : α ⊕ β) → γ ab), p fab) ↔ ∀ (fa : (val : α) → γ (Sum.inl val)) (fb : (val : β) → γ (Sum.inr val)), p fun (t : α ⊕ β) => Sum.rec fa fb t

source

@[simp]

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

Sum.inl (Sum.getLeft x h) = x

source

@[simp]

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

Sum.inr (Sum.getRight x h) = x

source

@[simp]

theorem Sum.getLeft?_eq_none_iff {α : Type u_1} {β : Type u_2} {x : α ⊕ β} :

Sum.getLeft? x = none ↔ Sum.isRight x = true

source

@[simp]

theorem Sum.getRight?_eq_none_iff {α : Type u_1} {β : Type u_2} {x : α ⊕ β} :

Sum.getRight? x = none ↔ Sum.isLeft x = true

source

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

x = Sum.inl (Sum.getLeft x h)

source

@[simp]

theorem Sum.getLeft_eq_iff :

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

source

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

x = Sum.inr (Sum.getRight x h)

source

@[simp]

theorem Sum.getRight_eq_iff :

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

source

@[simp]

theorem Sum.getLeft?_eq_some_iff :

∀ {α : Type u_1} {a : α} {β : Type u_2} {x : α ⊕ β}, Sum.getLeft? x = some a ↔ x = Sum.inl a

source

@[simp]

theorem Sum.getRight?_eq_some_iff :

∀ {β : Type u_1} {b : β} {α : Type u_2} {x : α ⊕ β}, Sum.getRight? x = some b ↔ x = Sum.inr b

source

@[simp]

theorem Sum.bnot_isLeft {α : Type u_1} {β : Type u_2} (x : α ⊕ β) :

(!decide (Sum.isLeft x = Sum.isRight x)) = true

source

@[simp]

theorem Sum.isLeft_eq_false {α : Type u_1} {β : Type u_2} {x : α ⊕ β} :

Sum.isLeft x = false ↔ Sum.isRight x = true

source

theorem Sum.not_isLeft {α : Type u_1} {β : Type u_2} {x : α ⊕ β} :

¬Sum.isLeft x = true ↔ Sum.isRight x = true

source

@[simp]

theorem Sum.bnot_isRight {α : Type u_1} {β : Type u_2} (x : α ⊕ β) :

(!decide (Sum.isRight x = Sum.isLeft x)) = true

source

@[simp]

theorem Sum.isRight_eq_false {α : Type u_1} {β : Type u_2} {x : α ⊕ β} :

Sum.isRight x = false ↔ Sum.isLeft x = true

source

theorem Sum.not_isRight {α : Type u_1} {β : Type u_2} {x : α ⊕ β} :

¬Sum.isRight x = true ↔ Sum.isLeft x = true

source

theorem Sum.isLeft_iff :

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

source

theorem Sum.isRight_iff :

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

source

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

Sum.inl a = Sum.inl b ↔ a = b

source

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

Sum.inr a = Sum.inr b ↔ a = b

source

theorem Sum.inl_ne_inr :

∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β}, Sum.inl a ≠ Sum.inr b

source

theorem Sum.inr_ne_inl :

∀ {β : Type u_1} {b : β} {α : Type u_2} {a : α}, Sum.inr b ≠ Sum.inl a

`Sum.elim` #

source

@[simp]

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

Sum.elim f g ∘ Sum.inl = f

source

@[simp]

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

Sum.elim f g ∘ Sum.inr = g

source

@[simp]

theorem Sum.elim_inl_inr {α : Type u_1} {β : Type u_2} :

Sum.elim Sum.inl Sum.inr = id

source

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)

source

@[simp]

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

Sum.elim (f ∘ Sum.inl) (f ∘ Sum.inr) = f

`Sum.map` #

source

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

source

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

source

@[simp]

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

Sum.map id id = id

source

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

source

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

source

@[simp]

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

Sum.isLeft (Sum.map f g x) = Sum.isLeft x

source

@[simp]

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

Sum.isRight (Sum.map f g x) = Sum.isRight x

source

@[simp]

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

Sum.getLeft? (Sum.map f g x) = Option.map f (Sum.getLeft? x)

source

@[simp]

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

Sum.getRight? (Sum.map f g x) = Option.map g (Sum.getRight? x)

`Sum.swap` #

source

@[simp]

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

Sum.swap (Sum.swap x) = x

source

@[simp]

theorem Sum.swap_swap_eq {α : Type u_1} {β : Type u_2} :

Sum.swap ∘ Sum.swap = id

source

@[simp]

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

Sum.isLeft (Sum.swap x) = Sum.isRight x

source

@[simp]

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

Sum.isRight (Sum.swap x) = Sum.isLeft x

source

@[simp]

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

Sum.getLeft? (Sum.swap x) = Sum.getRight? x

source

@[simp]

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

Sum.getRight? (Sum.swap x) = Sum.getLeft? x

source

theorem Sum.LiftRel.mono :

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

source

theorem Sum.LiftRel.mono_left :

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

source

theorem Sum.LiftRel.mono_right :

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

source

theorem Sum.LiftRel.swap :

∀ {α : Type u_1} {α_1 : Type u_2} {r : α → α_1 → Prop} {β : Type u_3} {β_1 : Type u_4} {s : β → β_1 → Prop} {x : α ⊕ β} {y : α_1 ⊕ β_1}, Sum.LiftRel r s x y → Sum.LiftRel s r (Sum.swap x) (Sum.swap y)

source

@[simp]

theorem Sum.liftRel_swap_iff :

∀ {β : Type u_1} {β_1 : Type u_2} {s : β → β_1 → Prop} {α : Type u_3} {α_1 : Type u_4} {r : α → α_1 → Prop} {x : α ⊕ β} {y : α_1 ⊕ β_1}, Sum.LiftRel s r (Sum.swap x) (Sum.swap y) ↔ Sum.LiftRel r s x y

source

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

Sum.Lex r s a b

source

theorem Sum.liftRel_subrelation_lex :

∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop}, Subrelation (Sum.LiftRel r s) (Sum.Lex r s)

source

theorem Sum.Lex.mono :

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

source

theorem Sum.Lex.mono_left :

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

source

theorem Sum.Lex.mono_right :

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

source

theorem Sum.lex_acc_inl :

∀ {α : Type u_1} {r : α → α → Prop} {a : α} {β : Type u_2} {s : β → β → Prop}, Acc r a → Acc (Sum.Lex r s) (Sum.inl a)

source

theorem Sum.lex_acc_inr :

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

source

theorem Sum.lex_wf :