Factoring through a sum of functions #
Sum.elim g₁ g₂ factors through Sum.elim f₁ f₂ exactly when each component factors
through its own and the two agree wherever f₁ and f₂ coincide: the factoring counterpart
of Function.Injective.sumElim.
[UPSTREAM] candidate for Mathlib/Data/Sum/Basic.lean, beside Function.Injective.sumElim.
theorem
Function.FactorsThrough.sumElim
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{f₁ : α → γ}
{f₂ : β → γ}
{g₁ : α → δ}
{g₂ : β → δ}
(h₁ : FactorsThrough g₁ f₁)
(h₂ : FactorsThrough g₂ f₂)
(h : ∀ (a : α) (b : β), f₁ a = f₂ b → g₁ a = g₂ b)
:
FactorsThrough (Sum.elim g₁ g₂) (Sum.elim f₁ f₂)
theorem
Function.factorsThrough_sumElim_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{f₁ : α → γ}
{f₂ : β → γ}
{g₁ : α → δ}
{g₂ : β → δ}
:
FactorsThrough (Sum.elim g₁ g₂) (Sum.elim f₁ f₂) ↔ FactorsThrough g₁ f₁ ∧ FactorsThrough g₂ f₂ ∧ ∀ (a : α) (b : β), f₁ a = f₂ b → g₁ a = g₂ b
The sum of two functions factors through the sum of two others exactly when each factors through its own and the two agree wherever the latter coincide.