English
For any families f1, f1', f2, f2', g1, g1', g2, g2' and any a = a_left ⊕ a_right and b = b_left ⊕ b_right, the element inr(c2) belongs to sumLexLift(f1,f2,g1,g2) a b exactly when either a is from the left and b from the right with c2 coming from g2 on (a1,b2), or a is from the right and b from the right with c2 coming from f2 on (a2,b2).
Русский
Для любых семей f1, f1', f2, f2', g1, g1', g2, g2' и любых a = inl a1 ⊕ inr a2, b = inl b1 ⊕ inr b2, элемент inr(c2) принадлежит sumLexLift(f1,f2,g1,g2) a b тогда и только тогда либо a = inl a1 и b = inr b2 и c2 ∈ g2 a1 b2, либо a = inr a2 и b = inr b2 и c2 ∈ f2 a2 b2.
LaTeX
$$$inr\ c_2 \in \mathrm{sumLexLift}(f_1,f_2,g_1,g_2)\ a\ b \iff (\exists a_1\, b_2,\ a = \mathrm{inl}(a_1) \land b = \mathrm{inr}(b_2) \land c_2 \in g_2 a_1 b_2) \lor (\exists a_2\, b_2,\ a = \mathrm{inr}(a_2) \land b = \mathrm{inr}(b_2) \land c_2 \in f_2 a_2 b_2)$$$
Lean4
theorem inr_mem_sumLexLift {c₂ : γ₂} :
inr c₂ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
(∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂ :=
by simp [mem_sumLexLift]
