Documentation

Std.Data.Sum.Lemmas

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 :
∀ {α : Type u_1} {r : α → α → Prop} {α_1 : Type u_2} {s : α_1 → α_1 → Prop}, WellFounded r → WellFounded s → WellFounded (Sum.Lex r s)
source
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
source
@[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