English
Define a lift sumLexLift that combines four maps f1, f2, g1, g2 to a map from α₁ ⊕ α₂ to β₁ ⊕ β₂ with Finset γ₁ ⊕ γ₂, by case distinction on the sum indices.
Русский
Определение lift sumLexLift, объединяющее четыре отображения f1, f2, g1, g2 в отображение из α₁ ⊕ α₂ в β₁ ⊕ β₂ на Finset (γ₁ ⊕ γ₂) с разбиением по случаям суммы.
LaTeX
$$sumLexLift : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂) defined by cases$$
Lean4
/-- Lifts maps `α₁ → β₁ → Finset γ₁`, `α₂ → β₂ → Finset γ₂`, `α₁ → β₂ → Finset γ₁`,
`α₂ → β₂ → Finset γ₂` to a map `α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)`. Could be generalized to
alternative monads if we can make sure to keep computability and universe polymorphism. -/
def sumLexLift : α₁ ⊕ α₂ → β₁ ⊕ β₂ → Finset (γ₁ ⊕ γ₂)
| inl a, inl b => (f₁ a b).map Embedding.inl
| inl a, inr b => (g₁ a b).disjSum (g₂ a b)
| inr _, inl _ => ∅
| inr a, inr b => (f₂ a b).map ⟨_, inr_injective⟩
