Function.Injective.sum_map
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)
The theorem `Function.Injective.sum_map` states that for any two types `α` and `α'`, and any two other types `β` and `β'`, if you have a function `f` that maps `α` to `β` and another function `g` that maps `α'` to `β'`, then, if both `f` and `g` are injective functions (meaning that for each one, identical outputs imply identical inputs), the function `Sum.map f g` that maps the sum type `α ⊕ α'` to `β ⊕ β'` is also injective. In other words, if you apply the `Sum.map f g` function to two distinct elements of the sum type `α ⊕ α'`, you will get distinct results in `β ⊕ β'`.
More concisely: If `f : α → β` and `g : α' → β'` are injective functions, then the function `Sum.map f g : α ⊕ α' → β ⊕ β'` is also injective.
|
Sum.inl_injective
theorem Sum.inl_injective : ∀ {α : Type u} {β : Type v}, Function.Injective Sum.inl
The theorem `Sum.inl_injective` states that for all types `α` and `β`, the function `Sum.inl` is injective. In other words, if we have two elements `a₁` and `a₂` from some type `α`, and if `Sum.inl a₁` equals `Sum.inl a₂`, then `a₁` must equal `a₂`. The function `Sum.inl` is a constructor for the sum type, which takes a value of type `α` and produces a value of the sum type `α ⊕ β`, tagged as coming from `α`. Being injective means it doesn't map different values to the same result.
More concisely: For all types `α` and `β`, the function `Sum.inl : α -> α ⊕ β` is an injection.
|
Sum.inr_injective
theorem Sum.inr_injective : ∀ {α : Type u} {β : Type v}, Function.Injective Sum.inr
The theorem `Sum.inr_injective` states that for any types `α` and `β`, the function `Sum.inr : β → α ⊕ β` (which sends each element of `β` to itself in the right component of the sum type `α ⊕ β`) is injective. This means that if `Sum.inr b₁ = Sum.inr b₂` for some `b₁, b₂ : β`, then it must be the case that `b₁ = b₂`.
More concisely: The function `Sum.inr : β -> α ⊕ β` is a injection (or equivalently, distinct elements of `β` map to distinct elements of `α ⊕ β` under `Sum.inr`).
|