Disjoint union of types #
Theorems about the definitions introduced in Init.Data.Sum.Basic.
@[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?
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 : Sum.LiftRel r₁ s₁ x y)
:
Sum.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 : Sum.LiftRel r₁ s x y)
:
Sum.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 : Sum.LiftRel r s₁ x y)
:
Sum.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 : Sum.LiftRel r s x y)
:
Sum.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 : α✝¹ ⊕ β✝¹}
:
Sum.LiftRel s r x.swap y.swap ↔ Sum.LiftRel r s x y
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
theorem
Sum.liftRel_subrelation_lex
{α✝ : Type u_1}
{r : α✝ → α✝ → Prop}
{β✝ : Type u_2}
{s : β✝ → β✝ → Prop}
:
Subrelation (Sum.LiftRel r s) (Sum.Lex r s)
theorem
Sum.lex_wf
{α✝ : Type u_1}
{r : α✝ → α✝ → Prop}
{α✝¹ : Type u_2}
{s : α✝¹ → α✝¹ → Prop}
(ha : WellFounded r)
(hb : WellFounded s)
:
WellFounded (Sum.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