support_indicator_subset

Mathlib.Data.Finsupp.Indicator

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

← MathLib Explorer

English

The support of indicator s f is contained in s: supp(indicator s f) ⊆ s.

Русский

Поддержка indicator s f содержится в s: supp(indicator s f) ⊆ s.

LaTeX

$$$\\operatorname{supp}(\\operatorname{indicator}(s,f)) \\subseteq s$$$

Lean4

theorem support_indicator_subset : ((indicator s f).support : Set ι) ⊆ s :=
  by
  intro i hi
  rw [mem_coe, mem_support_iff] at hi
  by_contra h
  exact hi (indicator_of_notMem h _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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