English
The cardinality of sigmaLift f a b is either the cardinality of f(a,b) if a and b share the same index, or 0 otherwise.
Русский
Кардинальность sigmaLift f a b равна кардинальности f(a,b), если a и b имеют одинаковый индекс, иначе 0.
LaTeX
$$$$ \mathrm{card}(\sigmaLift f a b) = \operatorname{ite} (a.fst = b.fst)\, (\mathrm{card}(f a b))\, 0 $$$$
Lean4
theorem card_sigmaLift : (sigmaLift f a b).card = dite (a.1 = b.1) (fun h => (f (h ▸ a.2) b.2).card) fun _ => 0 :=
by
simp_rw [sigmaLift]
split_ifs with h <;> simp