Function to Sum decomposition

Here we decompose a function f : α → β₁ ⊕ β₂ into a function and two bijections: α → α₁ ⊕ α₂ ≃ β₁ ⊕ β₂

def Function.decomposeSum {α β₁ β₂ : Type} (f : α → β₁ ⊕ β₂) : α ≃ { x₁ : α × β₁ // f x₁.1 = Sum.inl x₁.2 } ⊕ { x₂ : α × β₂ // f x₂.1 = Sum.inr x₂.2 }

Given f : α → β₁ ⊕ β₂ decompose α into two preïmages.

Equations

• One or more equations did not get rendered due to their size.

theorem Function.eq_comp_decomposeSum {α β₁ β₂ : Type} (f : α → β₁ ⊕ β₂) : f = Sum.elim (Sum.inl ∘ fun (x : { x₁ : α × β₁ // f x₁.1 = Sum.inl x₁.2 }) => (↑x).2) (Sum.inr ∘ fun (x : { x₂ : α × β₂ // f x₂.1 = Sum.inr x₂.2 }) => (↑x).2) ∘ ⇑(Function.decomposeSum f)