English
Definition: sumLift₂ lifts maps f and g to a map on sums, with empty cases when mixing left and right components.
Русский
Определение: sumLift₂ поднимает отображения f и g на суммы, с пустыми случаями при смешивании левых и правых компонент.
LaTeX
$$$\text{sumLift}_2(a,b) = \begin{cases} (f\ a\ b).map \mathrm{Embedding.inl}, & a,b \text{ both in left}, \\ \emptyset, & a\text{ left}, b\text{ right or vice versa}, \\ (g\ a\ b).map \mathrm{Embedding.inr}, & a,b \text{ both in right} \end{cases}$$$
Lean4
/-- Lifts maps `α₁ → β₁ → Finset γ₁` and `α₂ → β₂ → Finset γ₂` to a map
`α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)`. Could be generalized to `Alternative` functors if we can
make sure to keep computability and universe polymorphism. -/
@[simp]
def sumLift₂ : ∀ (_ : α₁ ⊕ α₂) (_ : β₁ ⊕ β₂), Finset (γ₁ ⊕ γ₂)
| inl a, inl b => (f a b).map Embedding.inl
| inl _, inr _ => ∅
| inr _, inl _ => ∅
| inr a, inr b => (g a b).map Embedding.inr
