English
The sumLexLift a b equals the empty set exactly when all the sub-families on the corresponding slices are empty: f1 on the left-left slice, g1,g2 on the left-right slice, and f2 on the right-right slice are all empty.
Русский
Сумма sumLexLift равна пустому множество тогда и только тогда все соответствующие подмножества пустые: f1 на левом левом срезе, g1,g2 на левом правом срезе и f2 на правом правом срезе пусты.
LaTeX
$$$\mathrm{sumLexLift}(f_1,f_2,g_1,g_2) a b = \emptyset \iff (\forall a_1,b_1, a = inl(a_1) \rightarrow b = inl(b_1) \rightarrow f_1 a_1 b_1 = \emptyset) \land (\forall a_1,b_2, a = inl(a_1) \rightarrow b = inr(b_2) \rightarrow g_1 a_1 b_2 = \emptyset \land g_2 a_1 b_2 = \emptyset) \land (\forall a_2,b_2, a = inr(a_2) \rightarrow b = inr(b_2) \rightarrow f_2 a_2 b_2 = \emptyset)$$$
Lean4
theorem sumLexLift_eq_empty :
sumLexLift f₁ f₂ g₁ g₂ a b = ∅ ↔
(∀ a₁ b₁, a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
(∀ a₁ b₂, a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
∀ a₂ b₂, a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅ :=
by
refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ ?_⟩
any_goals rintro a b rfl rfl; exact map_eq_empty.1 h
· rintro a b rfl rfl; exact disjSum_eq_empty.1 h
cases a <;> cases b
· exact map_eq_empty.2 (h.1 _ _ rfl rfl)
· simp [h.2.1 _ _ rfl rfl]
· rfl
· exact map_eq_empty.2 (h.2.2 _ _ rfl rfl)
