card_Icc — Mathlib

English

cardinality of the sigma-lifted Ico set equals the fiber Ico cardinality when the first components match, else zero.

Русский

Мощность множества Ico над сигма-типом равна мощности Ico в волокне, если первые компоненты совпадают; иначе - 0.

LaTeX

$$$\\#(Ico a b) = \\operatorname{if} h : a.\\mathrm{fst} = b.\\mathrm fst \\ \\operatorname{then} \\#(Ico (Eq.rec a.2 h) b.2) \\operatorname{else} 0$$$

Lean4

theorem card_Icc : #(Icc a b) = if h : a.1 = b.1 then #(Icc (h.rec a.2) b.2) else 0 :=
  card_sigmaLift (fun _ => Icc) _ _

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