English
sigmaLift f a b is nonempty precisely when a and b have the same index and the corresponding f(a,b) is nonempty.
Русский
sigmaLift f a b непуст тогда и только тогда, когда a и b имеют одинаковый индекс, и соответствующее f(a,b) непусто.
LaTeX
$$$$ \sigmaLift f a b \neq \emptyset \;\iff\; \exists h : a.1 = b.1, (f (h \|> a.2) b.2).\text{Nonempty} $$$$
Lean4
theorem sigmaLift_nonempty : (sigmaLift f a b).Nonempty ↔ ∃ h : a.1 = b.1, (f (h ▸ a.2) b.2).Nonempty :=
by
simp_rw [nonempty_iff_ne_empty, sigmaLift]
split_ifs with h <;> simp [h]