rangeIcc_support

Mathlib.Data.Finsupp.Interval

URI: https://scilib.ai/kg/mathlib#Finsupp.rangeIcc_support

English

The support of rangeIcc f g equals the union of the supports: supp(rangeIcc f g) = supp(f) ∪ supp(g).

Русский

Опора rangeIcc f g равна объединению опор f и g.

LaTeX

$$$\\operatorname{supp}(\\mathrm{rangeIcc}(f,g)) = \\operatorname{supp}(f) \\cup \\operatorname{supp}(g)$$$

Lean4

@[simp]
theorem rangeIcc_support (f g : ι →₀ α) : (rangeIcc f g).support = f.support ∪ g.support :=
  rfl

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

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

Разделы

Аффилиация

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