English
Detailed membership criterion for sumLexLift, listing all four disjunctive cases for a,b,c.
Русский
Детальная характеристика членства в sumLexLift, перечисляющая все четыре случая для a,b,c.
LaTeX
$$c ∈ sumLexLift f1 f2 g1 g2 a b ↔ (∃ a1 b1 c1, a = inl a1 ∧ b = inl b1 ∧ c = inl c1 ∧ c1 ∈ f1 a1 b1) ∨ (∃ a1 b2 c1, a = inl a1 ∧ b = inr b2 ∧ c = inl c1 ∧ c1 ∈ g1 a1 b2) ∨ (∃ a1 b2 c2, a = inl a1 ∧ b = inr b2 ∧ c = inr c2 ∧ c2 ∈ g2 a1 b2) ∨ (∃ a2 b2 c2, a = inr a2 ∧ b = inr b2 ∧ c = inr c2 ∧ c2 ∈ f2 a2 b2)$$
Lean4
theorem inl_mem_sumLexLift {c₁ : γ₁} :
inl c₁ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
(∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨ ∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂ :=
by simp [mem_sumLexLift]
