English
The sumLexLift expression is nonempty exactly when one of three cases occurs: (i) left-left with a nonempty f1, (ii) left-right with nonempty g1 or g2 on the left, or (iii) right-right with a nonempty f2 on the right.
Русский
Выражение sumLexLift непусто тогда, когда выполняется один из трёх случаев: (i) левая часть и f1 непусты, (ii) левая часть и левая правой части имеют непустые g1 или g2, или (iii) правая часть и f2 непусты.
LaTeX
$$$\mathrm{sumLexLift}(f_1,f_2,g_1,g_2) a b \neq \emptyset \iff (\exists a_1,b_1, a = inl(a_1) \land b = inl(b_1) \land (f_1 a_1 b_1).Nonempty) \lor (\exists a_1,b_2, a = inl(a_1) \land b = inr(b_2) \land ((g_1 a_1 b_2).Nonempty \lor (g_2 a_1 b_2).Nonempty)) \lor (\exists a_2,b_2, a = inr(a_2) \land b = inr(b_2) \land (f_2 a_2 b_2).Nonempty)$$$
Lean4
theorem sumLexLift_nonempty :
(sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
(∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
(∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty :=
by simp only [nonempty_iff_ne_empty, Ne, sumLexLift_eq_empty, not_and_or, exists_prop, not_forall]
