card_Icc

Mathlib.Data.DFinsupp.Interval

URI: https://scilib.ai/kg/mathlib#DFinsupp.card_Icc

English

Icc f g equals the dfinsupp of the union of supports with coordinates Icc(f(i), g(i)).

Русский

Icc f g равен DFinsupp-у∈ (f.support ∪ g.support) с координатами Icc(f(i), g(i)).

LaTeX

$$Icc_eq : Icc f g = (f.support ∪ g.support).dfinsupp (f.rangeIcc g)$$

Lean4

theorem card_Icc : #(Icc f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) :=
  card_dfinsupp _ _

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

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

Разделы

Аффилиация

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