card_Ico

Mathlib.Data.Sigma.Interval

URI: https://scilib.ai/kg/mathlib#Sigma.card_Ico

English

see Sigma.card_Ico (same content as above with different naming).

Русский

см. Sigma.card_Ico (аналогично выше).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru