English
sumLift₂ f g a b is nonempty iff either the left-left or right-right component is nonempty according to which part of the sum a,b lie.
Русский
sumLift₂ f g a b непуст тогда, когда соответствующая левая или правая часть не пуста в зависимости от того, к каким компонентам относятся a и b.
LaTeX
$$sumLift₂ f g a b .Nonempty ⇔ (∃ a1 b1, a = inl a1 ∧ b = inl b1 ∧ (f a1 b1).Nonempty) ∨ ∃ a2 b2, a = inr a2 ∧ b = inr b2 ∧ (g a2 b2).Nonempty$$
Lean4
theorem sumLift₂_nonempty :
(sumLift₂ f g a b).Nonempty ↔
(∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f a₁ b₁).Nonempty) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (g a₂ b₂).Nonempty :=
by simp only [nonempty_iff_ne_empty, Ne, sumLift₂_eq_empty, not_and_or, not_forall, exists_prop]
