More theorems about the sum type
@[simp]
Check if a sum is inl and if so, retrieve its contents.
Equations
- (sum.inr _x).get_left = option.none
- (sum.inl a).get_left = option.some a
@[simp]
Check if a sum is inr and if so, retrieve its contents.
Equations
- (sum.inr b).get_right = option.some b
- (sum.inl _x).get_right = option.none
@[simp]
theorem
sum.elim_inl
{α : Type u_1}
{β : Type u_2}
{γ : Sort u_3}
(f : α → γ)
(g : β → γ)
(x : α) :
@[simp]
theorem
sum.elim_inr
{α : Type u_1}
{β : Type u_2}
{γ : Sort u_3}
(f : α → γ)
(g : β → γ)
(x : β) :
theorem
sum.elim_injective
{α : Type u_1}
{β : Type u_2}
{γ : Sort u_3}
{f : α → γ}
{g : β → γ} :
function.injective f → function.injective g → (∀ (a : α) (b : β), f a ≠ g b) → function.injective (sum.elim f g)
- inl : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) {a₁ a₂ : α}, ra a₁ a₂ → sum.lex ra rb (sum.inl a₁) (sum.inl a₂)
- inr : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) {b₁ b₂ : β}, rb b₁ b₂ → sum.lex ra rb (sum.inr b₁) (sum.inr b₂)
- sep : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) (a : α) (b : β), sum.lex ra rb (sum.inl a) (sum.inr b)
Lexicographic order for sum. Sort all the inl a before the inr b,
otherwise use the respective order on α or β.
theorem
sum.lex_wf
{α : Type u}
{β : Type v}
{ra : α → α → Prop}
{rb : β → β → Prop} :
well_founded ra → well_founded rb → well_founded (sum.lex ra rb)
@[simp]
@[simp]
theorem
function.injective.sum_map
{α : Type u}
{α' : Type w}
{β : Type v}
{β' : Type x}
{f : α → β}
{g : α' → β'} :
function.injective f → function.injective g → function.injective (sum.map f g)
theorem
function.surjective.sum_map
{α : Type u}
{α' : Type w}
{β : Type v}
{β' : Type x}
{f : α → β}
{g : α' → β'} :
function.surjective f → function.surjective g → function.surjective (sum.map f g)