English
sumLift₂ f g a b equals empty set iff each left-left and right-right case yields empty members accordingly.
Русский
sumLift₂ f g a b равно пустому множеству тогда и только тогда, когда соответствующие левые пары и правые пары дают пустые множества.
LaTeX
$$sumLift₂ f g a b = ∅ ⇔ (∀ a1 b1, a = inl a1 ∧ b = inl b1 → f a1 b1 = ∅) ∧ ∀ a2 b2, a = inr a2 ∧ b = inr b2 → g a2 b2 = ∅$$
Lean4
theorem sumLift₂_eq_empty :
sumLift₂ f g a b = ∅ ↔
(∀ a₁ b₁, a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧ ∀ a₂ b₂, a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅ :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
·
constructor <;>
· rintro a b rfl rfl
exact map_eq_empty.1 h
cases a <;> cases b
· exact map_eq_empty.2 (h.1 _ _ rfl rfl)
· rfl
· rfl
· exact map_eq_empty.2 (h.2 _ _ rfl rfl)
