card_sigmaLift — Mathlib

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

Похожие утверждения