Sum.inr_ne_inl
theorem Sum.inr_ne_inl : ∀ {β : Type u_1} {b : β} {α : Type u_2} {a : α}, Sum.inr b ≠ Sum.inl a
This theorem states that for any types `α` and `β`, and for any elements `a` of type `α` and `b` of type `β`, the sum type operation `Sum.inr b` (injecting `b` into the sum type from the right) is not equal to the sum type operation `Sum.inl a` (injecting `a` into the sum type from the left). In other words, it declares that elements from different summands of a sum type are distinct.
More concisely: For all types `α` and `β` and elements `a : α`, `b : β`, `Sum.inr b` and `Sum.inl a` are distinct summand injections of `Sum α β`.
|
Sum.map_id_id
theorem Sum.map_id_id : ∀ {α : Type u_1} {β : Type u_2}, Sum.map id id = id
The theorem `Sum.map_id_id` states that for any types `α` and `β`, the application of the `Sum.map` function with identity functions for both its arguments is itself an identity function. In other words, if you have a sum type of `α` and `β`, and you map each component of the sum type to itself (i.e., you don't change it), the overall effect is the same as if you hadn't done anything. This is analogous to the mathematical property that the identity function applied to any function results in the original function.
More concisely: For any types `α` and `β`, the function `Sum.map` with identity functions as arguments is the identity function on the sum type `α ⊕ β`.
|
Sum.map_map
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
The theorem `Sum.map_map` states that for any types `α', α'', β', β'', α, β`, and for any functions `f': α' → α''`, `g': β' → β''`, `f: α → α'`, `g: β → β'`, and for any value `x` of type `α ⊕ β`, applying the function `Sum.map` twice in a row is the same as applying it once with the composition of the two initial functions. In other words, mapping twice sequentially is the same as mapping once with the composite function. This is an example of the property of function composition in the context of sum types.
More concisely: For any sum types `α ⊕ β`, functions `f: α → α'`, `g: β → β'`, `f': α' → α''`, `g': β' → β''`, and values `x` of type `α ⊕ β`, `Sum.map (f' ∘ g) x = Sum.map (g') (Sum.map f x)`.
|
Sum.elim_const_const
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
The theorem `Sum.elim_const_const` states that for any type `α`, `β`, any sort `γ`, and any constant `c` of type `γ`, applying the `Sum.elim` function to the constant functions `Function.const α c` and `Function.const β c` (which, regardless of their input, always output `c`) is the same as the constant function `Function.const (α ⊕ β) c`. In other words, it doesn't matter if we construct a function on the sum type `α ⊕ β` by separately defining constant functions on `α` and `β`, or if we directly define a constant function on `α ⊕ β` - both approaches give us the same result.
More concisely: For any types `α` and `β` and constant `c`, applying `Sum.elim` to the constant functions `Function.const α c` and `Function.const β c` is equivalent to the constant function `Function.const (α + β) c`, where `+` denotes the sum type.
|
Sum.inl_ne_inr
theorem Sum.inl_ne_inr : ∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β}, Sum.inl a ≠ Sum.inr b
This theorem states that, for any types `α` and `β` and any elements `a` of `α` and `b` of `β`, the `Sum.inl a` is not equal to `Sum.inr b`. In other words, the left injection of an element into the sum type is never equal to the right injection of a different type. This is a fundamental property of disjoint union types in type theory.
More concisely: For any types `α` and `β` and elements `a : α` and `b : β`, `Sum.inl a` is not equal to `Sum.inr b`.
|
Sum.swap_swap
theorem Sum.swap_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), x.swap.swap = x
This theorem, named `Sum.swap_swap`, states that for all types `α` and `β` and for any value `x` of type `α ⊕ β` (a sum type which can be either a value of type `α` or a value of type `β`), applying the `Sum.swap` function twice to `x` yields `x` itself. In other words, it is stating that swapping the components of the sum type twice reverts back to the original sum type.
More concisely: For all types `α` and `β`, and for any `x` of type `α ⊕ β`, the application of `Sum.swap` twice to `x` equals `x`.
|
Sum.comp_elim
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)
The theorem `Sum.comp_elim` states that for any types `α`, `β`, `γ`, and `δ`, and for any functions `f : γ → δ`, `g : α → γ`, and `h : β → γ`, the composition of `f` with the function `Sum.elim g h` (which is defined on the sum type `α ⊕ β` and maps each `α` to `γ` via `g` and each `β` to `γ` via `h`) is equal to `Sum.elim (f ∘ g) (f ∘ h)`. This means that the functions `f` and `Sum.elim g h` commute, i.e., the order in which they are applied does not matter.
More concisely: For any types `α`, `β`, `γ`, `δ`, and functions `f : γ → δ`, `g : α → γ`, and `h : β → γ`, the function composition `f ∘ Sum.elim g h` equals `Sum.elim (f ∘ g) (f ∘ h)` on the sum type `α ⊕ β`.
|
Sum.LiftRel.lex
theorem Sum.LiftRel.lex :
∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {a b : α ⊕ β},
Sum.LiftRel r s a b → Sum.Lex r s a b
This theorem states that for any two types `α` and `β`, and any two relations `r` on `α` and `s` on `β`, and for any two elements `a` and `b` that are either of type `α` or `β` (i.e., in the sum type `α ⊕ β`), if `a` and `b` satisfy the `Sum.LiftRel` predicate with respect to relations `r` and `s`, then `a` and `b` satisfy the `Sum.Lex` relation with respect to the same relations `r` and `s`. In other words, this theorem is about the preservation of a relational property when moving from the `LiftRel` predicate to the `Lex` relation on sum types.
More concisely: If `a` and `b` satisfy the `Sum.LiftRel` relation with respect to relations `r` on `α` and `s` on `β`, then `a` and `b` satisfy the `Sum. Lex` relation with respect to `r` and `s`.
|