Function to Sum decomposition

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

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

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

Equations

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

def Function.decomposeSum_unexpand : Lean.PrettyPrinter.Unexpander

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 = ◩x₁.2 }) => (↑x).2) (Sum.inr ∘ fun (x : { x₂ : α × β₂ // f x₂.1 = ◪x₂.2 }) => (↑x).2) ∘ ⇑f.decomposeSum

noncomputable instance instFintypeSubtypeProdEqSumFstInlSnd_seymour {α β₁ β₂ : Type} [Fintype α] {f : α → β₁ ⊕ β₂} : Fintype { x₁ : α × β₁ // f x₁.1 = ◩x₁.2 }

Equations

• instFintypeSubtypeProdEqSumFstInlSnd_seymour = Fintype.ofInjective (fun (x : { x₁ : α × β₁ // f x₁.1 = ◩x₁.2 }) => (↑x).1) ⋯

noncomputable instance instFintypeSubtypeProdEqSumFstInrSnd_seymour {α β₁ β₂ : Type} [Fintype α] {f : α → β₁ ⊕ β₂} : Fintype { x₂ : α × β₂ // f x₂.1 = ◪x₂.2 }

Equations

• instFintypeSubtypeProdEqSumFstInrSnd_seymour = Fintype.ofInjective (fun (x : { x₂ : α × β₂ // f x₂.1 = ◪x₂.2 }) => (↑x).1) ⋯

theorem Function.decomposeSum_card_eq {α β₁ β₂ : Type} [Fintype α] (f : α → β₁ ⊕ β₂) : #{ x₁ : α × β₁ // f x₁.1 = ◩x₁.2 } + #{ x₂ : α × β₂ // f x₂.1 = ◪x₂.2 } = #α