card_Ioo — Mathlib

English

cardinality of the sigma-lifted Ioo equals the fiber Ioo cardinality when the first components match; otherwise zero.

Русский

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

LaTeX

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

Lean4

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

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