card_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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